Bisimulace

Bisimulace je v teoretické informatice relace ekvivalance mezi stavy přechodových systémů.

Intuitivně jsou dva systémy bisimulární pokud dokážou dorovnat své vzájemné tahy. V tomto smyslu vnější pozorovatel nedokáže dva bisimulární systémy rozlišit.

Neboť Kripkeho modely jsou zvláštním případem přechodových systémů, bisimulace se objevuje jako téma v modální logice.

[editovat] Formální definice

Mějme štítkovaný přechodový systém (S, Λ, →). Relace bisimulace je binární relace R přes S (to je R ⊆ S × S) taková že R i R^-1 jsou simulační předuspořádání.

Ekvivalentní definice následuje. R je bisimulace pokud pro každou dvojici prvků p, q v S, pokud (p,q) je v R potom pro všechny α v Λ, a pro všechny p' v S, pokud

$\begin{matrix} & \alpha & \\ p & \rightarrow & p' \\ \end{matrix}$

pak existuje q' v S takové že

$\begin{matrix} & \alpha & \\ q & \rightarrow & q' \\ \end{matrix}$

a (p',q') je v R, a pro každé q' v S, a (p',q') je v R.

Pro dva stavy p a q v S, p je bisimilární ke q, psáno p ∼ q, pokud existuje bisimulace R taková že (p, q) je v R.

Relace bisimulace ∼ je relace ekvivalence. Dále je to největší relace bisimulace na daném přechodovém systému.

Ne nutně platí, že pokud p simuluje q a q simuluje p pak jsou bisimilární. Aby p a q byly bisimilární, simulace mezi p a q musí být inverze k simulaci mezi q a p.

[editovat] Varianty bisimulace

Pojem bisimulace je někdy zjemněn přidáním dalších požadavků či omezení. Proto se může obsah výrazu bisimulace v různých kontextech nepatrně lišit.

Například pro přechodové systémy vybavené tichou akcí, běžně značenou τ, to je akcí neviditelnou pro vnější pozorovatele, může být bisimulace oslabena za definice slabé bisimulace, ve které jsou tiché akce ignorovány.

Pokud přechodový systém slouží pro definici operační sémantiky programovacího jazyka, pak přesná definice bisimulace může být specifická k omezením daného programovacího jazyka.

[editovat] Rozhodnutelnost bisimulace

Bisimulace je rozhodnutelná pro následující druhy procesů.

bezkontextové procesy (známé také jako BPA procesy)^[1]
základní souběžné procesy (známé také jako BPP procesy)^[2]
normované procesy procesní algebry (PA)^[3]

[editovat] Reference

↑ Bisimulation Equivalence is Decidable for all Context-Free Processes — Søren Christensen, Hans Hüttel, Colin Stirling (anglicky)
↑ Strong Bisimilarity on Basic Parallel Processes is PSPACE-complete — Petr Jančar (anglicky)
↑ Bisimulation equivalence is decidable for normed Process Algebra — Yoram Hirshfeld and Mark Jerrum (anglicky)

Kategorie: Logika

Bisimulace v jiných jazycích: Deutsch, English, Français, 日本語

Tento článek je převzat z české wikipedie - otevřené encyklopedie, originální článek naleznete na adrese: „http://cs.wikipedia.org/wiki/Bisimulace“
Stránka byla naposledy upravena v Stránka byla naposledy editována 1. 12. 2007 v 14:10.
Veškerý text je dostupný za podmínek GNU Free Documentation License (Autorské právo pro podrobnosti).