Bisimulace
Definice
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 je relace bisimulace mezi a , pokud:
Když , pak musí platit následující tři podmínky:
- atomická harmonie
- "tam"
- "zpět"
Řekneme, že a jsou bisimilární, když existuje bisimulace taková, že .
Vlastnosti bisimulace
- je reflexivní
Identická relace je bisimulace z do .
, tudíž
- je symetrická
Když je bisimulace z do , tak je bisimulace z do .
- je tranzitivní
Když je bisimulace z 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 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 je bisimulace.
Zdroje
- Blackburn P., de Rijke M., Venema Y. Modal Logic. Cambridge University Press. (2002).
- Arazim P. Relace bisimulace (bakalářská práce). (2009).