Bisimulace: Porovnání verzí
| (Není zobrazeno 5 mezilehlých verzí 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 /> | ||
| + | Když <math>B(w,x)</math>, pak musí platit následující tři podmínky: | ||
| + | * atomická harmonie | ||
| + | <math>\forall p (w {\Vdash_1} p \Longleftrightarrow x {\Vdash_2} p)</math> | ||
| + | * "tam" | ||
| + | <math>w{R_1}w' \Rightarrow \exists x'(x{R_2}x' \wedge B(w', x'))</math> | ||
| + | * "zpět" | ||
| + | <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 <math>B</math> taková, že <math>B(w,x)</math>. | |
| − | + | == Vlastnosti bisimulace == | |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
* je '''reflexivní''' <br /> | * je '''reflexivní''' <br /> | ||
| − | Identická relace je bisimulace z | + | Identická relace je bisimulace z <math>\mathbb{M}</math> do <math>\mathbb{M}</math>. <br /> |
| − | + | <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ž | + | 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ž | + | 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).] | ||
| − | + | [[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ž , 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 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 .
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 .
, 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 , 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 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}
.
- 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).