====== 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> a přidáme <math>\wedge Sng(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]]