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/15 09:00]
lachmanfrantisek
+++ mgr-szz:in-pos:10-pos [2020/04/12 16:56]
@@ Řádek 1: / Řádek 1: @@
-====== IN-POS 10. Konečné automaty (FA) a logiky nad slovy ======
-===== Zadání =====
-  * Logika 1.řádu (FOL) a monadická logika 2.řádu (MSOL):
-    * syntax a sémantika FOL a MSOL,
-    * principy převoditelnosti mezi FA a formulemi MSOL.
-  * Automaty nad nekonečnými slovy a omega-regulární jazyky.
-  * IA006
-===== Vypracování =====
-==== Logika prvního řádu (FOL) nad slovy ====
-<note tip>
-FOL obecně je zpracována v jiné otázce:
-http://statnice.dqd.cz/home:inf:ap14
-</note>
-=== Syntax ===
-^ ^ ^
-|<m>x,y,z,...</m>| pozice|
-|<m>P_a(x)</m>|unární predikát značící, že na pozici <m>x</m> je písmeno ''a''|
-|<m>x < y</m>|pozice <m>x</m> je před <m>y</m>|
-|<m>\wedge , ∨ , ¬ </m>|logické spojky|
-|<m>\forall x, \exists x</m>|kvantifikace|
-| |+ rovnost <m>x=y</m>|
-==== Monadická logika druhého řádu (MSO) nad slovy ====
-=== Syntax ===
-^ ^ ^
-|<m>x,y,z,...</m>|pozice|
-|<m>P_a(x)</m>|unární predikát značící, že na pozici <m>x</m> je písmeno ''a''|
-|<m>x < y</m>|pozice <m>x</m> je před <m>y</m>|
-|<m>\wedge , ∨ , ¬ </m>|logické spojky|
-|<m>\forall x, \exists x</m>|kvantifikace|
-|<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|
-Proměnné ve formuli mohou být:
-  * **vázané** pomocí kvantifikátoru
-  * **volné** (zpravidla píšeme za jméno formule)
-<box 90% red|Sentence>
-sentence = uzavřená formule = formule bez volných proměnných
-</box>
-=== Jazyky zadané sentencí MSO ===
-  * Sentence MSO <m>\phi</m> = vlastnost slov
-  * Slovo <math>w \in \Sigma^{\star}</math> vlastnost <math>\phi</math>:
-    * má: <math>w \vDash \phi</math>
-    * nemá: <math>w \nvDash \phi</math>
-  * <math>L(\phi) := \lbrace w \in \Sigma^{\star} | w \vDash \phi \rbrace </math>
-=== Valuace formulí ===
-Valuace přiřazuje hodnotu volným proměnným.
-==== Vztah FA a formulí MSOL ====
-<box 90% red>
-Regulární jazyky = jazyky definovatelné MSO.
-</box>
-=== Převod NFA na formuli MSO ===
-NFA <math>A = (Q, q_0, \rightarrow, F)</math> -> sentence MSO <math>\phi</math> t.ž. <math>L(A) = L(\phi)</math>
-<math>\phi :=</math>
-^ ^ ^
-|<math>\exists \lbrace X_q | q \in Q \rbrace : ( </math>| máme množinu pozic odpovídající stavům původního automatu|
-|<math>\forall x : (</math> | |
-|<math>\underset{q \in Q}{\vee} x \in X_q</math>| každá pozice odpovídá některému stavu |
-|<math>\wedge \underset{q \neq r \in Q}{\wedge} (x \in X_q \Rightarrow x \notin X_r)</math>| každá pozice neodpovídá dvěma různým stavům |
-|<math>)</math>| |
-|<math>\wedge \forall x : First(x) \Rightarrow \underset{a \in \Sigma, q_0 \overset{a}{\rightarrow} \-\ q}{\vee} P_a(x) \wedge x \in X_q </math>| první prvek odpovídá počátečnímu stavu |
-|<math>\wedge \forall x,y : Succ(x,y) \Rightarrow \underset{a \in \Sigma, q \overset{a}{\rightarrow} \-\ r}{\vee} x \in X_q \wedge P_a(x) \wedge y \in X_r</math>| definice přechodů |
-|<math>\wedge \forall x : Last(x) \Rightarrow \underset{q \in F}{\vee} x \in X_q </math>| poslední prvek odpovídá finálnímu stavu |
-|<math>)</math>| |
-//First, Succ, Last// jsou jednoduše definovatelná makra
-<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>.
-  * 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.txt · Poslední úprava: 2020/04/12 16:56 (upraveno mimo DokuWiki)

Nahoru