Bisimulace

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

Mějme dva Kripkovské modely 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}_1 = (W_1, R_1, V_1)} a 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=(W_2, R_2, V_2)} .
Řekneme, že 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\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 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}_1}
 do $\mathbb {M} _{2}$ a 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_2}
 je bisimulace z $\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 $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).