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 /> | |
| − | + | 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 == | |
| − | |||
| − | |||
* 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).] | ||
| − | + | [[Kategorie: Modální logiky]] | |
| − | |||
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
- BLACKBURN Patrick, de RIJKE Maarten, VENEMA Yde. Modal Logic. Cambridge University Press. (2002).
- ARAZIM Pavel. Relace bisimulace (bakalářská práce). (2009).