Bisimulace

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

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⁻¹ 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

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

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

• bezkontextové procesy (známé také jako BPA procesy)
• základní souběžné procesy (známé také jako BPP procesy)
• normované procesy procesní algebry (PA)

Reference

Autoritní data	GND: 4619739-4