Bisimulace

Z Wikipedie, otevřené encyklopedie
Skočit na: Navigace, Hledání

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

Intuitivně jsou dva systémy bisimilární, pokud dokážou dorovnat své vzájemné tahy. V tomto smyslu vnější pozorovatel nedokáže dva bisimilá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.

Formální definice[editovat | editovat zdroj]

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.

Varianty bisimulace[editovat | editovat zdroj]

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.

Rozhodnutelnost bisimulace[editovat | editovat zdroj]

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]

Reference[editovat | editovat zdroj]

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