Bisimulace: Porovnání verzí

(Založena nová stránka s textem „== Bisimulace == === Definice === Bisimulace je binární relace ekvivalence mezi dvěma sémantickými modely. <br /> Mějme dva Kripkovská sémanti…“)
 
 
(Není zobrazeno 8 mezilehlých verzí od 2 dalších uživatelů.)
Řádek 1: Řádek 1:
== Bisimulace ==
+
'''Bisimulace''' je binární [[Ekvivalence|relace ekvivalence]] mezi dvěma sémantickými modely. <br /><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>.<br />
=== Definice ===
+
Řekneme, že <math>B\subseteq {W_1} \times {W_2}</math> je relace bisimulace mezi <math>\mathbb{M}_1</math> a <math>\mathbb{M}_2</math>, pokud: <br /><br />
 
+
Když <math>B(w,x)</math>, pak musí platit následující tři podmínky:
Bisimulace je binární relace ekvivalence mezi dvěma sémantickými modely. <br />
+
* atomická harmonie
 
+
     <math>\forall p (w {\Vdash_1} p \Longleftrightarrow x {\Vdash_2} p)</math>
Mějme dva [[Kripkovská sémantika|Kripkovské modely]] $\mathbb{M}_1 = (W_1, R_1, V_1)$ a $\mathbb{M}_2=(W_2, R_2, V_2)$.
+
* "tam"
Řekneme, že $B\subseteq {W_1} \times {W_2}$ je relace bisimulace mezi $\mathbb{M}_1$ a $\mathbb{M}_2$, pokud: <br />
+
     <math>w{R_1}w' \Rightarrow \exists x'(x{R_2}x' \wedge B(w', x'))</math>
 
+
* "zpět"  
Když $B(w,x)$, pak musí platit následující tři podmínky:
+
     <math>x{R_2}x' \Rightarrow \exists w'(w{R_2}w' \wedge B(w', x'))</math>
# 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'))$$Relace
 
# "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 ===
 
  
 +
Ř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 ==
 
* je '''reflexivní''' <br />
 
* je '''reflexivní''' <br />
   Identická relace je bisimulace z $\mathbb{M}$ do $\mathbb{M}$. <br />
+
   Identická relace je bisimulace z <math>\mathbb{M}</math> do <math>\mathbb{M}</math>. <br />
   $Id=\{(x,x)|x\in W\}$, tudíž $\mathbb{M}, x \underline{\leftrightarrow} \mathbb{M}, x$
+
   <math>Id=\{(x,x)|x\in W\}</math>, tudíž <math>\mathbb{M}, x \underline{\leftrightarrow} \mathbb{M}, x</math>
 
* je '''symetrická''' <br />
 
* je '''symetrická''' <br />
   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$.
+
   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ž $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.
+
   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 ==
 +
# BLACKBURN Patrick, de RIJKE Maarten, VENEMA Yde. Modal Logic. Cambridge University Press. (2002).
 +
# [https://is.cuni.cz/webapps/zzp/detail/74476/ ARAZIM Pavel. Relace bisimulace (bakalářská práce). (2009).]
  
# Blackburn P., de Rijke M., Venema Y. Modal Logic. Cambridge University Press. (2002).
+
[[Kategorie: Modální logiky]]
# [https://is.cuni.cz/webapps/zzp/detail/74476/ Arazim P. Relace bisimulace (bakalářská práce). (2009).]
 

Aktuální verze z 16. 9. 2014, 04:09

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 Patrick, de RIJKE Maarten, VENEMA Yde. Modal Logic. Cambridge University Press. (2002).
  2. ARAZIM Pavel. Relace bisimulace (bakalářská práce). (2009).