Bisimulace: Porovnání verzí

 
(Není zobrazena jedna mezilehlá verze od jednoho dalšího uživatele.)
Řádek 1: Řádek 1:
 
+
'''Bisimulace''' je binární [[Ekvivalence|relace ekvivalence]] mezi dvěma sémantickými modely. <br /><br />
=== Definice ===
+
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 />
 
+
Ř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 />
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>.
 
Ř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 />
 
 
 
 
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
Řádek 16: Řádek 11:
  
 
Ř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>.
 
Ř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 ===
 
 
 
 
* je '''reflexivní''' <br />
 
* je '''reflexivní''' <br />
 
   Identická relace je bisimulace z <math>\mathbb{M}</math> do <math>\mathbb{M}</math>. <br />
 
   Identická relace je bisimulace z <math>\mathbb{M}</math> do <math>\mathbb{M}</math>. <br />
Řádek 29: Řádek 22:
  
 
== 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, 03:09

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

Mějme dva Kripkovské modely Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_1 = (W_1, R_1, V_1)} a Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_2=(W_2, R_2, V_2)} .
Řekneme, že Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle B\subseteq {W_1} \times {W_2}} je relace bisimulace mezi Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_1} a Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_2} , pokud:

Když Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle B(w,x)} , pak musí platit následující tři podmínky:

  • atomická harmonie
   Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \forall p (w {\Vdash_1} p \Longleftrightarrow x {\Vdash_2} p)}

  • "tam"
   Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle w{R_1}w' \Rightarrow \exists x'(x{R_2}x' \wedge B(w', x'))}

  • "zpět"
   Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle x{R_2}x' \Rightarrow \exists w'(w{R_2}w' \wedge B(w', x'))}

Řekneme, že Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle (\mathbb{M}_1,w)} a Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle (\mathbb{M}_2,x)} jsou bisimilární, když existuje bisimulace Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle B} taková, že Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle B(w,x)} .

Vlastnosti bisimulace

  • je reflexivní
 Identická relace je bisimulace z Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}}
 do Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}}
. 
Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle Id=\{(x,x)|x\in W\}} , tudíž Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}, x \underline{\leftrightarrow} \mathbb{M}, x}
  • je symetrická
 Když Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle B\subseteq {W_1}\times{W_2}}
 je bisimulace z Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_1}
 do Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_2}
, tak Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \breve{B}=\{(x,w)|B(w,x)\}}
 je bisimulace z Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_2}
 do .
  • je tranzitivní
 Když Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle B_1}
 je bisimulace z Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_1}
 do Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_2}
 a Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle B_2}
 je bisimulace z Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_2}
 do Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \mathbb{M}_3}
,

pak Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle 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).