hledat
Rozdíly
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 13:26] lachmanfrantisek čístá MSO |
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é MSO** (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á" MSO** je ekvivalentní **MSO**. | ||
| - | * Pro zápis čisté MSO v MSO máme makra pro syntaxi, která v MSO není. | ||
| - | * Pro zápis MSO v čísté MSO nahradíme všechny prvořádové proměnné <math>x</math> druhořádovou proměnnou <math>S_x</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]] | ||
