Bisimulace

Bisimulace je binární relace ekvivalence mezi dvěma sémantickými modely.

Mějme dva Kripkovské modely $\mathbb {M} _{1}=(W_{1},R_{1},V_{1})$ a $\mathbb {M} _{2}=(W_{2},R_{2},V_{2})$.
Řekneme, že $B\subseteq {W_{1}}\times {W_{2}}$ je relace bisimulace mezi $\mathbb {M} _{1}$ a $\mathbb {M} _{2}$, pokud:

Když $B(w,x)$, pak musí platit následující tři podmínky:

• atomická harmonie

   $\forall p(w{\Vdash _{1}}p\Longleftrightarrow x{\Vdash _{2}}p)$

• "tam"

   $w{R_{1}}w'\Rightarrow \exists x'(x{R_{2}}x'\wedge B(w',x'))$

• "zpět"

   $x{R_{2}}x'\Rightarrow \exists w'(w{R_{2}}w'\wedge B(w',x'))$

Řekneme, že $(\mathbb {M} _{1},w)$ a $(\mathbb {M} _{2},x)$ jsou bisimilární, když existuje bisimulace $B$ taková, že $B(w,x)$.

Vlastnosti bisimulace

• je reflexivní
  

 Identická relace je bisimulace z $\mathbb {M}$ do $\mathbb {M}$. 

 $Id=\{(x,x)|x\in W\}$, tudíž $\mathbb {M} ,x{\underline {\leftrightarrow }}\mathbb {M} ,x$

• je symetrická
  

 Když $B\subseteq {W_{1}}\times {W_{2}}$ je bisimulace z $\mathbb {M} _{1}$ do $\mathbb {M} _{2}$, tak ${\breve {B}}=\{(x,w)|B(w,x)\}$ je bisimulace z $\mathbb {M} _{2}$ do $\mathbb {M} _{1}$.

• je tranzitivní
  

 Když $B_{1}$ je bisimulace z $\mathbb {M} _{1}$ do $\mathbb {M} _{2}$ a $B_{2}$ je bisimulace z $\mathbb {M} _{2}$ do $\mathbb {M} _{3}$,

pak $B_{1}\circ B_{2}=\{({w_{1}},{w_{2}})|\exists {w_{2}}({w_{1}}{B_{1}}{w_{2}}\wedge {w_{2}}{B_{2}}{w_{3}})\}$ je bisimulace.

Zdroje

1. BLACKBURN Patrick, de RIJKE Maarten, VENEMA Yde. Modal Logic. Cambridge University Press. (2002).
2. ARAZIM Pavel. Relace bisimulace (bakalářská práce). (2009).