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
	proměnné druhého řádu (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 \vDash \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
$)$

First, Succ, Last jsou jednoduše definovatelná makra

Dle slidů je někde chybka..;-(

Využijeme čisté MSOL (logika bez prvního řádu):


$X,Y,Z,...$	proměnné jen druhého řádu (množiny pozic)
$P_a(X)$	unární predikát značící, že na všech pozicách z $X$ je písmeno `a`
$X \subseteq Y$	$X$ je podmnožinou $Y$
$X$ < $Y$	něco z $X$ je před $Y$
$\wedge , \vee , \neg$	logické spojky
$\exists X$	kvantifikace (jen 2. řád)
$Sng(X)$	$\mid X \mid = 1$

„Č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é $x$ druhořádovou proměnnou $S_x$ a přidáme $\wedge Sng(S_x)$ .

1. zakódujeme valuace MSOL
- pro formuli s k proměnnými půjde o k+1-tici
- $w_v \in (\Sigma \times \lbrace 0,1 \rbrace^k)^{\star}$
2. máme překlad pro jednotlivé výrazy MSOL
- začínáme u podformulí a spojujeme dohromady

Složitost
- NFA → MSOL: $\mid\phi\mid = poly (\mid A\mid)$
- MSOL → NFA: $\mid A \mid = 2^{2^{\cdot^{\cdot^{2^{\mid\phi\mid}}}}} = 2^{O(\mid\phi\mid)}$

Jazyky akceptované:

Jazyky jsou uzavřeny na:

$\cap$ a $\cup$ .
doplněk
- Jazyky akceptované deterministickým BA nejsou uzavřeny na doplněk ⇒ det. BA nepopisují celou třídu omega-regulárních jazyků.