Bisimulace: Porovnání verzí

Řádek 1: Řádek 1:
 
  
 
=== Definice ===
 
=== Definice ===
  
Bisimulace je binární [[Ekvivalence|relace ekvivalence]] mezi dvěma sémantickými modely. <br />
+
Bisimulace je binární [[Ekvivalence|relace ekvivalence]] mezi dvěma sémantickými modely. <br />
  
 
Mějme dva [[Kripkovská sémantika|Kripkovské modely]] <math>\mathbb{M}_1 = (W_1, R_1, V_1)</math> a <math>\mathbb{M}_2=(W_2, R_2, V_2)</math>.
 
Mějme dva [[Kripkovská sémantika|Kripkovské modely]] <math>\mathbb{M}_1 = (W_1, R_1, V_1)</math> a <math>\mathbb{M}_2=(W_2, R_2, V_2)</math>.
Řádek 10: Řádek 9:
 
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>
  
Řekneme, že <math>(\mathbb{M}_1,w)</math> a <math>(\mathbb{M}_2,x)</math> jsou '''bisimilární''', když existuje bisimulace B taková, že <math>B(w,x)</math>.
+
Řekneme, že <math>(\mathbb{M}_1,w)</math> a <math>(\mathbb{M}_2,x)</math> jsou '''bisimilární''', když existuje bisimulace <math>B</math> taková, že <math>B(w,x)</math>.
 
      
 
      
 
=== Vlastnosti bisimulace ===
 
=== Vlastnosti bisimulace ===

Verze z 10. 9. 2014, 13:03

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