Zde můžete vidět rozdíly mezi vybranou verzí a aktuální verzí dané stránky.
Obě strany předchozí revize Předchozí verze Následující verze | Předchozí verze | ||
mgr-szz:in-pos:10-pos [2019/06/11 10:11] lachmanfrantisek FOL, MSOL |
mgr-szz:in-pos:10-pos [2020/04/12 16:56] (aktuální) |
||
---|---|---|---|
Řádek 40: | Řádek 40: | ||
|<m>\wedge , ∨ , ¬ </m>|logické spojky| | |<m>\wedge , ∨ , ¬ </m>|logické spojky| | ||
|<m>\forall x, \exists x</m>|kvantifikace| | |<m>\forall x, \exists x</m>|kvantifikace| | ||
- | |<m>X,Y,Z,...</m>| množiny pozic| | + | |<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>x \in X</m>| <m>x</m> leží v <m>X</m>| | ||
|<m>\forall X, \exists X</m>| kvantifikace nad množinami pozic| | |<m>\forall X, \exists X</m>| kvantifikace nad množinami pozic| | ||
Řádek 56: | Řádek 56: | ||
* Sentence MSO <m>\phi</m> = vlastnost slov | * Sentence MSO <m>\phi</m> = vlastnost slov | ||
- | * Slovo <m>w \in \Sigma^{\star}</m> vlastnost<m>\phi</m>: | + | * Slovo <math>w \in \Sigma^{\star}</math> vlastnost <math>\phi</math>: |
- | * má: <m>w</m> {{:mgr-szz:in-pos:vdash.png?25|}} <m>\phi</m> | + | * má: <math>w \vDash \phi</math> |
- | * nemá: <m>w</m> {{:mgr-szz:in-pos:nvdash.png?25|}} <m>\phi</m> | + | * nemá: <math>w \nvDash \phi</math> |
- | * <m>L(\phi) := \lbrace w \in \Sigma^{star} | w</m> {{:mgr-szz:in-pos:vdash.png?25|}} <m>\phi \rbrace</m> | + | * <math>L(\phi) := \lbrace w \in \Sigma^{\star} | w \vDash \phi \rbrace </math> |
Řádek 74: | Řádek 74: | ||
=== Převod NFA na formuli MSO === | === 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 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 ===== | ===== Zdroje ===== | ||
* [[http://www.fi.muni.cz/usr/kretinsky/MSO_Automaty_slides.pdf|slidy: V. Brožek: Logika a regulární jazyky]] | * [[http://www.fi.muni.cz/usr/kretinsky/MSO_Automaty_slides.pdf|slidy: V. Brožek: Logika a regulární jazyky]] |