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 $ \mathbb{M}_2 $, pokud:

Když $ B(w,x) $, pak musí platit následující tři podmínky:

  • atomická harmonie
   $ \forall p (w {\Vdash_1} p \Longleftrightarrow x {\Vdash_2} p) $
  • "tam"
   $ w{R_1}w' \Rightarrow \exists x'(x{R_2}x' \wedge B(w', x')) $
  • "zpět"
   $ x{R_2}x' \Rightarrow \exists w'(w{R_2}w' \wedge B(w', x')) $

Řekneme, že $ (\mathbb{M}_1,w) $ a $ (\mathbb{M}_2,x) $ jsou bisimilární, když existuje bisimulace $ B $ taková, že $ B(w,x) $.

Vlastnosti bisimulace

  • je reflexivní
 Identická relace je bisimulace z $ \mathbb{M} $ do $ \mathbb{M} $. 
$ Id=\{(x,x)|x\in W\} $, tudíž $ \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 $ \mathbb{M}_2 $, tak $ \breve{B}=\{(x,w)|B(w,x)\} $ je bisimulace z $ \mathbb{M}_2 $ do $ \mathbb{M}_1 $.
  • je tranzitivní
 Když $ B_1 $ je bisimulace z $ \mathbb{M}_1 $ do $ \mathbb{M}_2 $ a $ B_2 $ je bisimulace z $ \mathbb{M}_2 $ do $ \mathbb{M}_3 $,

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