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
- BLACKBURN Patrick, de RIJKE Maarten, VENEMA Yde. Modal Logic. Cambridge University Press. (2002).
- ARAZIM Pavel. Relace bisimulace (bakalářská práce). (2009).