Bisimulace

Definice

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

Mějme dva Kripkovské modely Nelze pochopit (syntaktická chyba): {\displaystyle $\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:

  1. atomická harmonie
   $$\forall p (w {\Vdash_1} p \Longleftrightarrow x {\Vdash_2} p)$$
  1. "tam"
   $$w{R_1}w' \Rightarrow \exists x'(x{R_2}x' \wedge B(w', x'))$$Relace
  1. "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 P., de Rijke M., Venema Y. Modal Logic. Cambridge University Press. (2002).
  2. Arazim P. Relace bisimulace (bakalářská práce). (2009).