hledat
Rozdíly
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 13:26] lachmanfrantisek čístá MSO |
mgr-szz:in-pos:10-pos [2020/04/12 16:56] (aktuální) |
||
|---|---|---|---|
| Řádek 59: | Řádek 59: | ||
| * má: <math>w \vDash \phi</math> | * má: <math>w \vDash \phi</math> | ||
| * nemá: <math>w \nvDash \phi</math> | * nemá: <math>w \nvDash \phi</math> | ||
| - | * <math>L(\phi) := \lbrace w \in \Sigma^{\star} | w \nvDash \phi \rbrace </math> | + | * <math>L(\phi) := \lbrace w \in \Sigma^{\star} | w \vDash \phi \rbrace </math> |
| Řádek 98: | Řádek 98: | ||
| - | Využijeme **čisté MSO** (logika bez prvního řádu): | + | Využijeme **čisté MSOL** (logika bez prvního řádu): |
| ^ ^ ^ | ^ ^ ^ | ||
| Řádek 109: | Řádek 109: | ||
| |<math>Sng(X)</math>|<math>\mid X \mid = 1</math>| | |<math>Sng(X)</math>|<math>\mid X \mid = 1</math>| | ||
| - | * **"Čistá" MSO** je ekvivalentní **MSO**. | + | * **"Čistá" MSOL** je ekvivalentní **MSOL**. |
| - | * Pro zápis čisté MSO v MSO máme makra pro syntaxi, která v MSO není. | + | * Pro zápis čisté MSOL v MSOL máme makra pro syntaxi, která v MSOL 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>. | + | * 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]] | ||
