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 Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}}
 do $\mathbb {M}$. 

 $Id=\{(x,x)|x\in W\}$, tudíž Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \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 Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_2}
 do Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_3}
,

pak Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle 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).