Bisimulace

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

Mějme dva Kripkovské modely a Nelze pochopit (Chyba konverze. Server („https://en.wikipedia.org/api/rest_“) hlásí: „Cannot get mml. Server problem.“): {\displaystyle \mathbb {M} _{2}=(W_{2},R_{2},V_{2})} .
Řekneme, že Nelze pochopit (Chyba konverze. Server („https://en.wikipedia.org/api/rest_“) hlásí: „Cannot get mml. Server problem.“): {\displaystyle B\subseteq {W_{1}}\times {W_{2}}} je relace bisimulace mezi a Nelze pochopit (Chyba konverze. Server („https://en.wikipedia.org/api/rest_“) hlásí: „Cannot get mml. Server problem.“): {\displaystyle \mathbb {M} _{2}} , pokud:

Když Nelze pochopit (Chyba konverze. Server („https://en.wikipedia.org/api/rest_“) hlásí: „Cannot get mml. Server problem.“): {\displaystyle B(w,x)} , pak musí platit následující tři podmínky:

  • atomická harmonie
   
  • "tam"
   Nelze pochopit (Chyba konverze. Server („https://en.wikipedia.org/api/rest_“) hlásí: „Cannot get mml. Server problem.“): {\displaystyle w{R_{1}}w'\Rightarrow \exists x'(x{R_{2}}x'\wedge B(w',x'))}

  • "zpět"
   Nelze pochopit (Chyba konverze. Server („https://en.wikipedia.org/api/rest_“) hlásí: „Cannot get mml. Server problem.“): {\displaystyle x{R_{2}}x'\Rightarrow \exists w'(w{R_{2}}w'\wedge B(w',x'))}

Řekneme, že a Nelze pochopit (Chyba konverze. Server („https://en.wikipedia.org/api/rest_“) hlásí: „Cannot get mml. Server problem.“): {\displaystyle (\mathbb {M} _{2},x)} jsou bisimilární, když existuje bisimulace taková, že Nelze pochopit (Chyba konverze. Server („https://en.wikipedia.org/api/rest_“) hlásí: „Cannot get mml. Server problem.“): {\displaystyle B(w,x)} .

Vlastnosti bisimulace

  • je reflexivní
 Identická relace je bisimulace z  do . 
Nelze pochopit (Chyba konverze. Server („https://en.wikipedia.org/api/rest_“) hlásí: „Cannot get mml. Server problem.“): {\displaystyle Id=\{(x,x)|x\in W\}} , tudíž
  • je symetrická
 Když Nelze pochopit (Chyba konverze. Server („https://en.wikipedia.org/api/rest_“) hlásí: „Cannot get mml. Server problem.“): {\displaystyle B\subseteq {W_{1}}\times {W_{2}}}
 je bisimulace z  do , tak Nelze pochopit (Chyba konverze. Server („https://en.wikipedia.org/api/rest_“) hlásí: „Cannot get mml. Server problem.“): {\displaystyle {\breve {B}}=\{(x,w)|B(w,x)\}}
 je bisimulace z  do .
  • je tranzitivní
 Když  je bisimulace z  do  a  je bisimulace z  do ,

pak 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).