Rozdíly

Zde můžete vidět rozdíly mezi vybranou verzí a aktuální verzí dané stránky.

--- mgr-szz:in-pos:10-pos [2019/06/11 11:39]
lachmanfrantisek převod NFA na sentenci MSO
+++ mgr-szz:in-pos:10-pos [2020/04/12 16:56] (aktuální)
@@ Řádek 40: / Řádek 40: @@
 |<m>\wedge , ∨ , ¬ </m>|logické spojky|
 |<m>\forall x, \exists x</m>|kvantifikace|
-|<m>X,Y,Z,...</m>| množiny pozic|
+|<m>X,Y,Z,...</m>| proměnné druhého řádu (množiny pozic)|
 |<m>x \in X</m>| <m>x</m> leží v <m>X</m>|
 |<m>\forall X, \exists X</m>| kvantifikace nad množinami pozic|
@@ Řádek 59: / Řádek 59: @@
     * má: <math>w \vDash \phi</math>
     * nemá: <math>w \nvDash \phi</math>
-  * <math>L(\phi) := \lbrace w \in \Sigma^{\star} | w \nvDash \phi \rbrace </math>
+  * <math>L(\phi) := \lbrace w \in \Sigma^{\star} | w \vDash \phi \rbrace </math>
@@ Řádek 75: / Řádek 75: @@
 === Převod NFA na formuli MSO ===
-==== Automaty nad nekonečnými slovy a omega-regulární jazyky ====
 NFA <math>A = (Q, q_0, \rightarrow, F)</math> -> sentence MSO <math>\phi</math> t.ž. <math>L(A) = L(\phi)</math>
@@ Řádek 96: / Řádek 94: @@
 <note important>Dle slidů je někde chybka..;-(</note>
+=== Převod sentence MSOL na NFA ===
+Využijeme **čisté MSOL** (logika bez prvního řádu):
+^ ^ ^
+|<math>X,Y,Z,...</math>| proměnné jen druhého řádu (množiny pozic)|
+|<math>P_a(X)</math>|unární predikát značící, že na všech pozicách z <math>X</math> je písmeno ''a''|
+|<math>X \subseteq Y</math>|<math>X</math> je podmnožinou <math>Y</math>|
+|<math>X</math> < <math>Y</math>|něco z <math>X</math> je před <math>Y</math>|
+|<math>\wedge , \vee , \neg </math>|logické spojky|
+|<math>\exists X</math>|kvantifikace (jen 2. řád)|
+|<math>Sng(X)</math>|<math>\mid X \mid = 1</math>|
+  * **"Čistá" MSOL** je ekvivalentní **MSOL**.
+    * Pro zápis čisté MSOL v MSOL máme makra pro syntaxi, která v MSOL není.
+    * Pro zápis MSOL v čísté MSOL nahradíme všechny prvořádové proměnné <math>x</math> druhořádovou proměnnou <math>S_x</math> a přidáme <math>\wedge Sng(S_x)</math>.
+  * 1. zakódujeme valuace **MSOL**
+    * pro formuli s  //k// proměnnými půjde o //k+1//-tici
+    * <math>w_v \in (\Sigma \times \lbrace 0,1 \rbrace^k)^{\star}</math>
+  * 2. máme překlad pro jednotlivé výrazy **MSOL**
+    * začínáme u podformulí a spojujeme dohromady
+  * Složitost
+    * NFA -> MSOL: <math>\mid\phi\mid = poly (\mid A\mid)</math>
+    * MSOL -> NFA: <math>\mid A \mid = 2^{2^{\cdot^{\cdot^{2^{\mid\phi\mid}}}}} = 2^{O(\mid\phi\mid)}</math>
+==== Automaty nad nekonečnými slovy a omega-regulární jazyky ====
+  * **Automaty**
+    * NFA A = <math>A = (Q, q_0, \rightarrow, Akc)</math>
+  * Por nekonečná slova máme rozdílné akceptační podmínky (<math>Inf(\rho)</math> značí stavy, které běh <math>\rho</math> navštíví <math>\infty</math>:
+    * **Büchi**
+      * <math>Akc = F \subseteq Q</math>
+      * cíl: <math>Inf(\rho) \cap F \neq \emptyset </math>
+    * **Muller**
+      * <math>Akc = \mathcal{F} \subseteq 2^Q</math>
+      * cíl: <math>Inf(\rho) \in \mathcal{F}</math>
+    * **Rabin**
+      * <math>Akc = \mathcal{T} \subseteq 2^Q \times 2^Q</math>
+      * cíl: <math>\exists(N,K) \in \mathcal{T} : N \cap Inf(\rho) \neq \emptyset \wedge K \cap Inf(\rho) = \emptyset </math>
+=== Omega-regulární jazyky ===
+Jazyky akceptované:
+  * nedeterministickými Büchiho automaty (BA)
+  * (ne)deterministickými Mullerovy automaty
+  * (ne)deterministickými Rabinovy automaty
+Jazyky jsou uzavřeny na:
+  * <math>\cap</math> a <math>\cup</math>.
+  * doplněk
+    * Jazyky akceptované deterministickým BA nejsou uzavřeny na doplněk => det. BA nepopisují celou třídu omega-regulárních jazyků.
 ===== Zdroje =====
   * [[http://www.fi.muni.cz/usr/kretinsky/MSO_Automaty_slides.pdf|slidy: V. Brožek: Logika a regulární jazyky]]

mgr-szz/in-pos/10-pos.1560245993.txt.gz · Poslední úprava: 2020/04/12 16:56 (upraveno mimo DokuWiki)

Nahoru