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 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} , pokud:

Když 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(w,x)} , pak musí platit následující tři podmínky:

• atomická harmonie

   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 \forall p (w {\Vdash_1} p \Longleftrightarrow x {\Vdash_2} p)}

• "tam"

   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 w{R_1}w' \Rightarrow \exists x'(x{R_2}x' \wedge B(w', x'))}

• "zpět"

   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 x{R_2}x' \Rightarrow \exists w'(w{R_2}w' \wedge B(w', x'))}

Ř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 (\mathbb{M}_1,w)} 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,x)} jsou bisimilární, když existuje bisimulace 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} taková, ž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(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 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}}
. 

 $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 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}
, tak ${\breve {B}}=\{(x,w)|B(w,x)\}$ 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}_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 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}
 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 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).