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 15:06] lachmanfrantisek převod MSOL na NFA |
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 \nvDash \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 ==== | ||
- | |||
- | ===== Zdroje ===== | ||
- | |||
- | * [[http://www.fi.muni.cz/usr/kretinsky/MSO_Automaty_slides.pdf|slidy: V. Brožek: Logika a regulární jazyky]] |