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

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

Syntax

x,y,z,... pozice
P_a(x)unární predikát značící, že na pozici x je písmeno a
x < ypozice x je před y
\wedge , ∨ , ¬logické spojky
\forall x, \exists xkvantifikace
+ rovnost x=y

Monadická logika druhého řádu (MSO) nad slovy

Syntax

x,y,z,...pozice
P_a(x)unární predikát značící, že na pozici x je písmeno a
x < ypozice x je před y
\wedge , ∨ , ¬logické spojky
\forall x, \exists xkvantifikace
X,Y,Z,... proměnné druhého řádu (množiny pozic)
x \in X x leží v X
\forall X, \exists X 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)

Sentence

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

Jazyky zadané sentencí MSO

  • 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 formulí

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

Vztah FA a formulí MSOL

Regulární jazyky = jazyky definovatelné MSO.

Převod NFA na formuli 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..;-(

Převod sentence MSOL na NFA

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 YX je podmnožinou Y
X < Yněco z X je před Y
\wedge , \vee , \neglogické spojky
\exists Xkvantifikace (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)}

Automaty nad nekonečnými slovy a omega-regulární jazyky

  • Automaty
    • NFA A = A = (Q, q_0, \rightarrow, Akc)
  • Por nekonečná slova máme rozdílné akceptační podmínky (Inf(\rho) značí stavy, které běh \rho navštíví \infty:
    • Büchi
      • Akc = F \subseteq Q
      • cíl: Inf(\rho) \cap F \neq \emptyset
    • Muller
      • Akc = \mathcal{F} \subseteq 2^Q
      • cíl: Inf(\rho) \in \mathcal{F}
    • Rabin
      • Akc = \mathcal{T} \subseteq 2^Q \times 2^Q
      • cíl: \exists(N,K) \in \mathcal{T} : N \cap Inf(\rho) \neq \emptyset \wedge K \cap Inf(\rho) = \emptyset

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:

  • \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ů.

Zdroje

mgr-szz/in-pos/10-pos.txt · Poslední úprava: 2020/04/12 16:56 (upraveno mimo DokuWiki)
Nahoru
CC Attribution-Noncommercial-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0