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.

FOL obecně je zpracována v jiné otázce:
http://statnice.dqd.cz/home:inf:ap14


	pozice
	unární predikát značící, že na pozici je písmeno `a`
	pozice je před
$\wedge , ∨ , ¬$	logické spojky
$\forall x, \exists x$	kvantifikace
	+ rovnost


	pozice
	unární predikát značící, že na pozici je písmeno `a`
	pozice je před
$\wedge , ∨ , ¬$	logické spojky
$\forall x, \exists x$	kvantifikace
	množiny pozic
$x \in X$	leží v
$\forall X, \exists X$	kvantifikace nad množinami pozic

Proměnné ve formuli mohou být:

Sentence

sentence = uzavřená formule = formule bez volných proměnných

Sentence MSO $\phi$ = vlastnost slov
Slovo $w \in \Sigma^{\star}$ vlastnost $\phi$ :
- má: $w \vDash \phi$
- nemá: $w \nvDash \phi$
$L(\phi) := \lbrace w \in \Sigma^{\star} | w \nvDash \phi \rbrace$

Valuace přiřazuje hodnotu volným proměnným.

Regulární jazyky = jazyky definovatelné MSO.

NFA $A = (Q, q_0, \rightarrow, F)$ → sentence MSO $\phi$ t.ž. $L(A) = L(\phi)$

$\phi :=$


$\exists \lbrace X_q \| q \in Q \rbrace : ($	máme množinu pozic odpovídající stavům původního automatu
$\forall x : ($
$\underset{q \in Q}{\vee} x \in X_q$	každá pozice odpovídá některému stavu
$\wedge \underset{q \neq r \in Q}{\wedge} (x \in X_q \Rightarrow x \notin X_r)$	každá pozice neodpovídá dvěma různým stavům
$)$
$\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$	první prvek odpovídá počátečnímu stavu
$\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$	definice přechodů
$\wedge \forall x : Last(x) \Rightarrow \underset{q \in F}{\vee} x \in X_q$	poslední prvek odpovídá finálnímu stavu
$)$