Bisimulace: Porovnání verzí

Řádek 8: Řádek 8:
  
 
Když <math>B(w,x)</math>, pak musí platit následující tři podmínky:
 
Když <math>B(w,x)</math>, pak musí platit následující tři podmínky:
# atomická harmonie
+
* atomická harmonie
 
     <math>\forall p (w {\Vdash_1} p \Longleftrightarrow x {\Vdash_2} p)</math>
 
     <math>\forall p (w {\Vdash_1} p \Longleftrightarrow x {\Vdash_2} p)</math>
# "tam"
+
* "tam"
 
     <math>w{R_1}w' \Rightarrow \exists x'(x{R_2}x' \wedge B(w', x'))</math>
 
     <math>w{R_1}w' \Rightarrow \exists x'(x{R_2}x' \wedge B(w', x'))</math>
# "zpět"  
+
* "zpět"  
 
     <math>x{R_2}x' \Rightarrow \exists w'(w{R_2}w' \wedge B(w', x'))</math>
 
     <math>x{R_2}x' \Rightarrow \exists w'(w{R_2}w' \wedge B(w', x'))</math>
  
Řádek 25: Řádek 25:
 
   Když <math>B\subseteq {W_1}\times{W_2}</math> je bisimulace z <math>\mathbb{M}_1</math> do <math>\mathbb{M}_2</math>, tak <math>\breve{B}=\{(x,w)|B(w,x)\}</math> je bisimulace z <math>\mathbb{M}_2</math> do <math>\mathbb{M}_1</math>.
 
   Když <math>B\subseteq {W_1}\times{W_2}</math> je bisimulace z <math>\mathbb{M}_1</math> do <math>\mathbb{M}_2</math>, tak <math>\breve{B}=\{(x,w)|B(w,x)\}</math> je bisimulace z <math>\mathbb{M}_2</math> do <math>\mathbb{M}_1</math>.
 
* je '''tranzitivní''' <br />
 
* je '''tranzitivní''' <br />
   Když <math>B_1</math> je bisimulace z <math>\mathbb{M}_1</math> do <math>\mathbb{M}_2</math> a <math>B_2</math> je bisimulace z <math>\mathbb{M}_2</math> do <math>\mathbb{M}_3</math>, pak <math>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})\}</math> je bisimulace.
+
   Když <math>B_1</math> je bisimulace z <math>\mathbb{M}_1</math> do <math>\mathbb{M}_2</math> a <math>B_2</math> je bisimulace z <math>\mathbb{M}_2</math> do <math>\mathbb{M}_3</math>,
 +
pak <math>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})\}</math> je bisimulace.
  
 
== Zdroje ==
 
== Zdroje ==

Verze z 10. 9. 2014, 14:04

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:

  • 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  a  je bisimulace z  do ,

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