Definice

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

Mějme dva Kripkovské modely a . Řekneme, že je relace bisimulace mezi a , pokud:

Když , pak musí platit následující tři podmínky:

  1. atomická harmonie
   :
  1. "tam"
   :
  1. "zpět"
   :

Řekneme, že a jsou bisimilární, když existuje bisimulace B 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  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  do , 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 P., de Rijke M., Venema Y. Modal Logic. Cambridge University Press. (2002).
  2. Arazim P. Relace bisimulace (bakalářská práce). (2009).