m FIMU Fakulta informatiky Masarykova univerzita Automaty nad nekonečnými slovy Mojmír Kfetínský Učební text FI MU Copyright © 2018, FI MU verze 1.0 prosinec 2018 Obsah 1 Biichiho automaty 3 1.1 Jazyky nekonečných slov 3 1.2 uj-automaty 4 1.3 Uzáverové vlastnosti Biichi-rozpoznatelných jazyků 8 1.4 Regulární Lj-jazyky 10 1.5 Komplementace Biichiho automatu a relace kongruence 1.6 Modiňkace Biichiho akceptačnípodmínky 16 2 Silnější akceptační podmínky 19 2.1 Mullerovy automaty 19 2.2 Rabínovy a Streettovy automaty 22 2.2.1 Rabínův automat 22 2.2.2 Streettův automat 24 OBSAH Kapitola 1 Biichiho automaty 1.1 Jazyky nekonečných slov Nechf S je konečná abeceda. S* značí množinu všech slov konečné délky, typicky označovaných u, v, w,... G S*, w = aoai... an, kde G S. Slovo nekonečné délky, nazývané též uj-slovo, definujeme jako funkci a : No —>• S. Symbolem S" značíme množinu všech slov nekonečné délky, typicky označovaných a,/3 ... G Eu. Tedy a (i) označuje písmeno na i—té pozici a cj-slovo a můžeme a často též budeme zapisovat jako a = a(0)a(í).... Dále označme S°° = S* U S". Pro přirozená m, n taková, že m < n definujeme a[m, n] = a(m)a(m + 1) . .. a(n) a[m, n) = a (m) a (m + 1) . .. a (n — 1) a[m, uj\ = a(m)a(m + 1) .. . V dalším textu použijeme pro kvantifikátory "existuje nekonečně mnoho n" a "existuje pouze konečně mnoho n" jako zkratky symboly resp. 3 i A 4>(n)) a dále 3(n) A 3Íij.{j > í ^(j)). Analogicky zápis V"n.(n) budeme interpretovat jako zkratku pro 3í.\/n.(n > i =>• (n)). Nechf ICS^ľC Pro x E X,y E Y definujeme jejich zřetězení jako slovo x.y = x(0)x(í)... x(n)y(0)y(í)..., kde x (í) = Xi (symbol '.' často vynecháváme, tj. místo x.y píšeme stručněji xy). Dále zřetězení jazyků ICE'aľC S°° definujeme jako jazyk X.Y = {x.y \ x e X, y e Y} a nekonečnou iteraci (w-iteraci) jazyka ICS* jako jazyk Xu = {xoXl ... \ x,eX- {e}} tj. Xu je množina všech nekonečných slov, která získáme zřetězením nekonečné posloupnosti neprázdných slov z X. Je-li například u = a0ai.. .an,a,i G X a X = {u}, pak Xu = {it"}, kde uu je nekonečné slovo aoai ... anaoai ... anao ..., které též můžeme zapsat jako uu ... . Pro Y = {x, y} je Y" = {xx ..., xy ... ,yx ... ,yy ..., ...}. 3 4 KAPITOLA 1. BŮCHIHO AUTOMATY Dále pro ICS* definujme pref(X) = {u e S* I 3«.to e X} lim(X) = {a G S" I 3"n.a[0,n] G X} , tj. a e \\m(X), právě když a má nekonečně mnoho prefixů v X. Poznamenejme, že často používanou notací pro li m (X) jsou též značení X či Xs. Operátory w-iterace a lim jsou oba typu S* —>• 2ľ", a tedy umožňují definovat nekonečná slova pomocí slov konečné délky. Příklad 1.1. (a) Je-li U = a*b, pak \\m(U) = 0. (b) Je-li U = (ab)+, pak \\m(U) = (ab)". (c) Je-li U = (a*b)+ = (a + b)*b, tj. U je množina všech slov končících symbolem b, pak \\m(U) = (a*b)u je množinou všech w-slov obsahujících nekonečně mnoho výskytu b. 1.2 w-automaty Přechodový systém A (s návěštími a počátečními stavy), zkráceně LTS (labelled transition systém) definujeme jako A = (S, S, A, Sin), kde S je množina stavů, S je konečná (vstupní) abeceda, A C S x S x 5je přechodová relace a 5in C S je množina počátečních stavů. Namísto (s, a, s') e A často píšeme s -°>a s', či pouze s A s', pokud je A zřejmá z kontextu. Někdy též mluvíme o přechodovém systému nad abecedou S a v tom případě jej zapisujeme pouze jako A = (S, A, Sin). Poznamejme, že takto definovaný LTS je obecně nedeterministický, mimo jiné proto, že A je relace, nikoliv funkce z S1 x S do S1. Přechodový systém A nazveme deterministický, jestliže card(Sin) = 1 apřechodová relace je funkcí A : S x S —>• S. V případě deterministických LTS lze bez újmy na obecnosti předpokládat, že A je totálni, tj. definovaná pro všechny argumenty (v opačném případě přidáme nový "záchytný" stav, do nějž vedeme všechny dosud nedefinované přechody; přechody z tohoto nově přidaného stavu vedou opět jen do tohoto stavu). Je-li u = a\d2 ■ ■ ■ am slovo nad S, pak klademe s A s', právě když existují s0, Si, ..., sm G S taková, že s = s0, si_1 —\ Sj (0 < i < m) a sm = s1. Běh LTS. Nechf A = (S, A, Sm) je LTS nad S, w G S*, w = a0ax ...an konečné vstupní slovo a a : No —>• S vstupní w-slovo. Běh p systému A na slově w je konečná posloupnost s0, si, ... s„+1 stavů z S taková, že Vz. 0 < i < m : s j ^\ Sj+i- Běh p systému A na w-slově a je definován jako nekonečná posloupnost p : No —>• S taková, že \fí .í e No : p(i) p(i + 1). Je-li navíc p(0) e Sin, resp. s0 e Sin nazýváme běh iniciálním. Běh je tedy posloupnost stavů, jimiž může A projít při postupném čtení slova dle pravidel přechodové relace. V dalším textu, pokud nebude řečeno jinak, budeme termínem běh rozumět iniciální běh, ostatní běhy nazveme neiniciální či obecné běhy. 1.2. uj-A UTOMATY 5 Dále pro libovolné w-slovo p : No —>• S klademe inf(p) = {s e S I 3"n. p (n) = s}, occ(p) = {s e S | 3n. p(n) = s} tedy inf (p) definujeme jako množinu symbolů z S, které se vyskytují v w-slově p nekonečně často, kdežto occ(er) je množina symbolů z S, které se v a vyskytují. w-automat. Nechf A = (S, A, Sin) je LTS nad £, pak w-automatem nazveme systém A = (A, Acc) , kde Acc je tzv. akceptační podmínka definující, kdy je w-slovo akceptováno, a to obvykle na základě existence běhu jistých vlastností na daném slově. Takový běh nazveme úspěšný nebo též akceptující. Poznamenejme, že w-automat je obecně nedeterministický, a tedy může pro w-slovo a existovat více vzájemně různých běhů. Je-li A konečně stavový, pak A nazveme konečným w-automatem. Pokud nebude v dalším textu řečeno jinak, budeme mít na mysli pouze konečné automaty (i když některé z dále uváděných výsledků platí i pro automaty nekonečné s nejvýše spočetnou množinu stavů). Řekneme, že w-automat A je deterministický, právě když jeho LTS A je deterministický. Biichiho automat. Nechf A = (S,A, 5j„) je LTS nad S. Řekneme, že w-automat (A, Acc) je Bůchiho automatem, právě když Acc je tzv. Bůchi akceptační podmínka (BAC): je dána konečná množina F C S akceptuj ich (též finálních) stavů a slovo a : No —>• S je akceptováno, právě když existuje běh p : No —>• S na slově a takový, že inf (p) n F ^ 0. V tomto případě říkáme, že A akceptuje a. Bůchiho podmínku můžeme stručněji zapsat takto: (BAC) 3p.(p(0) G Sm A \/i.{p{i) a-$ p(í + 1) G A) A inf (p) n F ^ 0 Uvedený Bůchiho automat A značíme (A, F) nebo též (S, S, A, 5j„, F). Jazyk rozpoznávaný (též akceptovaný) Bůchiho automatem A = (A, F) je množina L(Ä) = {a e S" I A akceptuje a} všech cj-slov akceptovaných tímto automatem a značíme jej též L(A, F). Konečně řekneme, že množina L C S" je rozpoznatelná ve smyslu Bůchiho (či Bůchi-rozpoznatelná), právě když existuje Bůchiho automat A takový, že L = L(A). Automaty A, B nazveme ekviva-letní, právě když L (A) = L(B). Obrázek 1.1: typický úspěšný běh Bůchiho automatu, s e Sin, / G F 6 KAPITOLA 1. BŮCHIHO AUTOMATY Poznámka 1.2. Bíichiho akceptační podmínka tedy požaduje, aby se nějaká podmnožina množiny F vyskytovala v úspěšném běhu p nekonečně častokrát: jelikož F je konečná, musí existovat nějaký stav / G F, který se v p vyskytuje nekonečněkrát. Pokud si představíme přechodový graf Bíichiho automatu, pak cesta tímto grafem koresponující úspěšnému běhu začíná v nějakém stavu z Sin, dosáhne stavu / a podél nějaké cesty se do / opět (nekonečně častokrát) vrací - viz též obrázek 1.1. □ Podmínku inf(p) n F ^ 0 (tj. VíBj.j > i : p(j) G F) z BAC kladenou na stavy úspěšného běhu p můžeme formálně zapsat jako formuli predikátového počtu prvního řádu takto: qeF Příklad 1.3. Mějme Bůchiho automaty A = ({qi, q2}, {a, b}, A, {gi}, {92}) , kde A je dána takto: a b qi ->• 92 qi ->• qi 92 A 91 q2 A qx a B = ({qi, q2}, {a, b}, A, {gi}, {g2}), kde A je dána takto: a qi 02 92 A gi g2 A gi Obrázek 1.2: Automaty .4 (vlevo) a B (vpravo) Automat A je deterministický a s totální přechodovou funkcí (resp. jeho přechodový systém má tyto vlastnosti); rovněž B je deterministický, ale jeho přechodová funkce je parciální (sestrojte ekvivalentní automat s totální A). Automat A akceptuje množinu všech w-slov takových, která obsahují nekonečně mnoho výskytů symbolu a, kdežto L(B) je tvořen všemi slovy, u nichž je každý sudý přechod pod písmenem a. Úkol: Sestrojte Bůchiho automat nad {a, b} akceptující množinu právě všech takových slov, v nichž se symboly a a b se vykytují nekonečně mnohokrát, přičemž mezi každými dvěma výskyty symbolu a je sudý počet výskytů symbolu b. Pro konečné automaty (FA) pracující nad slovy konečné délky platí, že nedetermi-nismus nezvětšuje vyjadřovací sílu, tj. ke každému nedeterministickému konečnému automatu (NFA) existuje ekvivaletní deterministický konečný automat (DFA). Zabývejme se nyní otázkou, zda platí tento vztah u Bůchiho automatů. 1.2. uj-A UTOMATY 7 Příklad 1.4. Nechť je dán Btichiho automat Ai = ({si, s2}, {», b}, Ai, {si}, {si}), kde Ai je dána takto: a b si ->• si si ->• s2 a s2 ->• Sl s2 ->• s2 a Btichiho automat _42 = ({si, s2}, {a, 6}, A2, {si}, {s2}), kde A2 je dána takto: a b b Si —>• Si Si —>• Si Si —>• S2 b «2 «2 a, b b Obrázek 1.3: Automaty Ai (vlevo) a A2 (vpravo) Automat A z přikladu 1.3 je ekvivalentní s výše uvedeným Ai - oba akceptují množinu všech w-slov obsahujících nekonečně mnoho výskytů symbolu a (zde však, na rozdíl od A, všechny a-přechody vedou do akceptujícího stavu si a současně všechny přechody do si jsou pod symbolem a). Automat _42 akceptuje množinu všech w-slov, která je komplementem L(A\). A2 je nedeterministický - uhodne místo ve vstupním slově, za nímž již nejsou žádné výskyty a. Taková pozice ve slově musí existovat, nebof libovolné vstupní slovo, které má být akceptováno, má jen konečně mnoho výskytů a. Automat pak kontroluje správnost svého hádání tím, že může číst pouze symboly b; z s2 totiž nevede žádný a-přechod a A2 by nebyl schopen pokračovat ve čtení vstupního slova, a tedy by jej nemohl akceptovat. □ Poznámka 1.5. Jak již bylo uvedeno, A z příkladu 1.3 a _4i z příkladu 1.4 jsou ekvivaletní. Jelikož v úspěšném běhu se musí symbol a vyskytovat nekonečně mnohokrát, není nutno, aby každý výskyt a byl zaznamenán průchodem přes akceptující stav - A prochází přes akceptující stavy jen při každém lichém výskytu symbolu a. Ve výše uvedeném příkladu 1.4 platí L(.42) = {a, b}* — L(A\). Povšimnněme si, že _4i je deterministický, ale A2 je nedeterministický. Ukážeme, že nedeterminismus je v tomto případě nevyhnutelný v tom smyslu, že neexistuje žádný deterministický Bůchiho automat, který by rozpoznával komplement jazyka L(A\). □ Věta 1.6. Jazyk L C S" je rozpoznatelný deterministickým Bůchiho automatem, právě když existuje regulárníjazykU C S* takový, že L = Iim(č7). Důkaz. ^^: Nechť U je regulární jazyk nad S. Pak existuje DFA A = (S, S, A, qo, F) takový, že L (A) = U. Pokud .4 interpretujeme jako Bůchiho automat, pak L(A) = Iim(č7) a protože přechodový systém automatu A se touto interpretací nezměnil, máme Bůchiho automat deterministický. 8 KAPITOLA 1. BŮCHIHO AUTOMATY =^>: Nechť L je rozpoznáván deterministickým Btichiho automatem A s množinou akceptuj ich stavů F. Pokud F interpretujeme jako množinu koncových stavů DFA s týmž přechodovým systémem jako má A, pak tento DFA akceptuje jistý regulární jazyk, řekněme U. Opět se snadno nahlédne, že L = Iim(č7). □ Důsledek 1.7. Existují jazyky rozpoznatelné nedeterministickými Biichiho automaty, které nejsou rozpoznatelné žádnými deterministickými Biichiho automaty. Důkaz. Ukážeme, že jazyk Ĺ = L(A2) z příkladu 1.4 není tvaru Iim(č7) pro žádný regulární jazyk U. Připomeňme, že Ĺ je množinou všech w-slov nad £ = {a, b}* obsahujících nekonečně mnoho výskytů symbolu b, ale pouze konečně mnoho výskytů symbolu a. Sporem. Předpokládejme, že L je rozpoznatelný deterministickým Bůchiho automatem. Pak dle Věty 1.6 existuje regulární U C S* nad takový, že Ĺ = Iim(č7). Jelikož bu G L, pak musí existovat jeho nějaký konečný prefix bni e U. Odtud a z definice jazyka Ĺ plyne, že bnrabM e L, a tedy opět musí existovat nějaký konečný prefix bniabn2 e U. Tedy opět z definice L plyne, že bni abn2 abM e L, a tudíž musí existovat další konečný prefix bni abn2 abns E U. Tímto postupem obdržíme nekonečnou posloupnost slov z U: {bni, bniabn2, bniabn2abna,... } C U . Z definice operátoru lim plyne, že i w-slovo /? = bniabn2abn3a ... abni ■ ■ ■ E lim(t/). Avšak f3 má nekonečně mnoho výskytů symbolu a, takže jistě nepatří do L, což je ale spor s předpokladem, že L = lim(t/). □ Ukázali jsme tedy, že třída jazyků rozpoznávaných deterministickými Bůchiho automaty je vlastní podtřídou jazyků rozpoznávaných nedeterministickými Bůchiho automaty. 1.3 Uzáverové vlastnosti Buchi-rozpoznatelných jazyků V této části se budeme zabývat studiem některých uzáverových vlastností Bůchi-rozpozna-telných jazyků. Všechny uvedené důkazy budou konstruktivní a uvedené techniky lze tedy použít pro návrh těchto automatů. Věta 1.8. Jsou-li L\, L2 C S" Búchi-rozpoznatelné jazyky, pak L\ U L2 a L\ n L2 jsou Bůchi-rozpoznatelné. Důkaz. Mějme Bůchiho automaty Ai = (Si, S, Aj, S*n, Fi) takové, že Li = L(Ai), i = 1,2. (a) Uzavřenost vůči sjednocení lze dokázat stejným postupem jako v případě nedeterministických konečných automatů: bez újmy na obecnosti lze předpokládat, že množiny stavů těchto automatů jsou disjunktní. Pak L\ U L2 je rozpoznáván automatem A = (Si U S2, S, Ai U A2, S}n U Sfn, Fi U F2). Počet stavů automatu A je tedy roven součtu počtu stavů automatů Ai. (b) Uzavřenost vůči průniku se v případě konečných automatů dokazuje konstrukcí automatu realizujícího tzv. synchronní paralelní spojení daných automatů - stavový prostor 1.3. UZÁVEROVÉ VLASTNOSTIBŮCHI-ROZPOZNATELNÝCH JAZYKŮ 9 automatu rozpoznávajího průnik je kartézským součinem stavových prostorů výchozích automatů a odpovídajícím způsobem jsou definovány i ostatní komponenty, například množina koncových stavů je opět kartézským součinem původních množin koncových stavů. Pro případ nekonečných slov však musíme uvedenou konstrukci poněkud upravit. Nekonečné slovo a má být akceptováno, jestliže každá z obou synchronních kopií Ai, i = 1, 2 prochází při běhu na slově a akceptujícími stavy nekonečně častokrát. Bohužel však není garantováno, že při takovém běhu by akceptující stavy obou automatů byly navštěvovány současně. Například jeden automat by procházel akceptujícími stavy po přečtení a(0) ,a(2),.. kdežto druhý po přečtení a(1), a(3),.... Tedy za množinu akceptujících stavů průnikového automatu nelze vzít ř\ x F2. Klíčovým pozorováním je fakt (viz poznámka 1.5), že nemusíme zaznamenávat každý výskyt, kdy každá z kopií navštěvuje své akceptující stavy. Stačí, aby každá z těchto kopií zanamenávala jen nekonečnou podposloupnost své původní posloupnosti akceptujících stavů. Jinak řečeno, začneme s tím, že u první kopie (komponenty) budeme čekat na průchod akceptujícím stavem a jakmile toto nastane, přeneseme svoji pozornost na očekávání výskytu akceptujícího stavu u druhé kopie; vejde-li tato do svého akceptujícího stavu, přepneme zpět na pozorování výskytu akceptujícího stavu u první kopie atd. Je vidět, že budeme přepínat mezi kopiemi nekonečně častokrát, právě když každá z kopií navštěvuje své akceptující stavy nekonečně častokrát. Automat rozpoznávající L\ n L2 lze tedy definovat jako A = (S, £, A, Sin, F), kde • S = S!xS2x {1,2}, • A je definována takto: (s1,s2,í) A (s'1; 4,1) je-li si A si e Ai, s2 A s'2 e A2, si ^ F1 (si,s2,l) A (si,sí,,2) je-li si A si e Ai, s2 A s'2 e A2, si G F1 (s1;s2,2) A (si,s2,2) je-li Sl A si e A1; s2 A s'2 e A2, s2 £ F2 (si,s2,2) A (si,s2,1) je-li si A si e Ai, s2 A s'2 e A2, s2 e F2, • Sin = {(si, s2,1) | si e S}n, s2 e Sfn}, • F = Sx x F2 x {2}. Uvedený automat akceptuje, jestliže přepíná z druhé do první komponenty nekonečně častokrát. Počet stavuje tedy úměrný součinu počtu stavů automatů Ai - Poznamenejme, že ekvivaletně jsme mohli při konstrukci A položit F = Fi x S2 x {1}). Snadno se ověří, že L (A) = L(Ai) n L(^l2). □ Věta 1.9. Nechi U C S* je regulární a L C Eu je Búchi-rozpoznatelný. Pak (i) Uu je Búchi-rozpoznatelný a (ii) U.L je Búchi-rozpoznatelný. Důkaz, (i) Bez újmy na obecnosti můžeme předpokládat, že U neobsahuje prázdné slovo (platí totiž, že U" = (U - {e})" ) a že konečný automat A = (S, S, A, q0, F) rozpoznávající U má jediný počáteční stav qo, do kterého nevedou žádné přechody. Bůchiho automat rozpoznávající U" je A' = (S, S, A', qo, {qo}), kde A' = A U {s A qo \ s A s',s' e F}. (ii) Bůchiho automat rozpoznávající zřetězení U.L se sestrojí analogicky jako pro případ konečných automatů. Formální popis konstrukce i důkaz její korektnosti je přenechán 10 KAPITOLA 1. BŮCHIHO AUTOMATY čtenáři. □ Poznámka 1.10. Uzavřenost vůči doplnku. Btichi-rozpoznatelné jazyky jsou uzavřeny i vůči operaci doplňku, avšak důkaz je obtížnější a bude mu věnována samostatná sekce. Jedním problémem je, že ke konstrukci nemůžeme použít deterministického Búchiho automatu (viz Důsledek 1.7). Druhým problémem je, že samotná Búchiho akceptační podmínka, tj. cyklus v přechodovém grafu automatu při úspěšném běhu na a, může mimo akceptující stavy z F obsahovat též stavy, které nejsou z F, a tudíž nahrazení F jeho komplementem by způsobilo, že a by bylo opět akceptováno. Tento problém bude pro nás (mimo jiné) motivací hledat "jemnějšf' akceptační podmínky (viz kapitola 2). Uzáverové vlastnosti deterministických Biichi-rozpoznatelných jazyků Řekneme, že jazyk L je deterministický Bůchi-rozpoznatelný, jestliže existuje deterministický Búchiho automat A takový, že L = L (A). Věta 1.11. Jsou-li Li, L2 C deterministické Btichi-rozpoznatelné jazyky, pak i jazyky L\ U L2 a L\ n L2JSOU deterministické Btichi-rozpoznatelné. Důkaz. Mějme deterministické Búchiho automaty Ai = (Si,T,, Aj, qi, Fi) takové, že Lí = L(Aí), i = 1,2. Uzavřenost vůči sjednocení: připomeňme (viz věta 1.6), že L je deterministický Bůchi-rozpoznatelný jazyk, právě když existuje U C S* taková, že L = Iim(č7). Tedy existují Ui C S* taková, že Li = \\m(Ui),i = 1,2. Tvrzení o existenci deterministického automatu okamžitě plyne ze vztahu lim(t/i U U2) = lim(t/i) U Iim(č72). Ke konstrukci odpovídajícího automatu A lze použít synchronního paralelního spojení automatů Ai s množinou koncových stavů F = F\ x S2 U S± x F2. Jelikož Ai jsou deterministické, je deterministický i A. Poznamenejme, že výsledný A má počet stavů roven součinu počtů stavů automatů Ai- Dále si všimněme, ke konstrukci A nelze použít konstrukci uvedenou v důkazu věty. 1.8 Uzavřenost vůči průniku lze dokázat užitím konstrukce z důkazu věty 1.8. Snadno se nahlédne, že pokud jsou dané Ai deterministické, pak i výsledný automat A je deterministický. □ 1.4 Regulární w-jazyky Pro zevrubnější analýzu Bůchi-rozpoznatelných jazyků budeme používat toto značení: je-li dán Búchiho automat A= (S, S, A, Sin, F), pak klademe Zřejmě každý z konečně mnoha jazyků Wss> je regulární (je rozpoznatelný nedeterministickým konečným automatem (S, S,A,{s},{s'}) ). Z definice Búchiho automatu (viz též poznámka 1.2) plyne, že w-jazyk rozpoznávaný automatem A je Wss, = {w e s* I s 4 s'}. (1.1) s0eSm,s£F 1.4. REGULÁRNÍ u-JAZYKY 11 Pokud by A byl (bez újmy na obecnosti) s jediným počátečním stavem so, pak L(A) = UseFWS0S.(Wssr . Věta 1.12. Libovolný uj-jazyk L C Eu je Biichi-rozpoznatelný, právě když je konečným sjednocením množin U.VU, kde U, V C S* jsou regulární množiny (konečných slov). Navíc lze bez újmy na obecnosti předpokládat, žeV.V C V. Důkaz. =^>: platnost této implikace okamžitě plyne ze vztahu (1.1); poznamenejme, že V.V C V plyne z WSS.WSS C Wss. plyne z uzavřenosti Btichi-rozpoznatelných jazyků vzhledem ke konečnému sjednocení, zřetězení a w-iteraci. □ Reprezentaci w-jazyka ve tvaru L = U™=i UiV", kde U i,Ví C £*, z = 1,..., n, jsou regulární výrazy, nazýváme w-regulárním výrazem. Řekneme, že jazyk L C lľ" je regulární w-jazyk (či stručněji je w-regulární), právě když L = UiLi UiV^, kde t/j, Ví C £*, z = 1,..., n, jsou regulární jazyky (konečných slov). Viz též následující poznámka 1.13 Zřejmě platí, že jazyk je w-regulární, právě když je popsán nějakým w-regulárním výrazem a právě když je Búchi-rozpoznatelný. Poznámka 1.13. V literatuře se lze setkat s několika definicemi w-regulárních jazyků, které jsou ekvivaletní s výše uvedenou definicí, která pro naše účely postačí (a je dostatečně jednoduchá). Jedná se například o algebraickou definici, kdy regularitu i w-regularitu lze definovat pomocí homomorfismu daného jazyka do konečného monoidu. Jiný přístup je založen na definici w-regulárních jazyků jako nejmenší množiny 1Z podmnožin S°° obsahující (i) prázdnou množinu, (ii) jednoprvkové množiny {a} pro každý symbol a e S a uzavřenou (iii) vůči konečnému sjednocení, zřetězení a (iv) iteracím (*-iterace a w-iterace) - viz definice zřetězení a w-iterace v části 1.1. Konečně poznamenejme, že pro termín regulární w-jazyk se též používají i termíny racionální či w-racionální jazyk (či již výše uvedené synonymum w-regulární jazyk). □ Řekneme, že w-slovo a e Eu má nekonečný periodický rozvoj (anglicky "is ulti-mately periodic"), jestliže existují u, v e S* taková, že a = uvvv .... Věta 1.14. (i) Libovolný neprázdný uj-regulární jazyk L obsahuje slovo s nekonečným periodickým rozvojem. (ii) Problém prázdnosti je pro Búchiho automaty rozhodnutelný. Důkaz. Tvrzení (i) plyne z rovnosti (1.1) takto: nechf L = L(A, F) pro nějaký Bůchiho automat (A, F). Pak a e L(A, F) je tvaru a = uviV2 ■ ■., kde sq ^ f a / ^> f pro všechna i > 1 a nějaká s0 e 5j„, / G F. Pak i slovo f3 = uviVi... e L(A, F) a f3 je periodické. Nyní ukážeme, že tvrzení (ii) opět plyne ze vztahu (1.1) a z existence algoritmu pro dosažitelnost akceptujícího stavu v nějaké netriviální (tj. alespoň jednu hranu obsahující) silně souvislé komponentě přechodového grafu Búchiho automatu. Mějme tedy dán libovolný Bůchiho automat A = (A, F). Pokud v přechodovém systému A = (S, S, A, Sin) tohoto automatu abstrahujeme od návěští hran, obdržíme ori- 12 KAPITOLA 1. BŮCHIHO AUTOMATY entovaný graf Ga = (S, E), kde (s, s') e E ^=h> 3a e S : s A s'. Z (1.1) zřejmě plyne, že L(A, F) ^ 0, právě když v G a existuje netriviální silně souvislá komponenta X taková, že X obsahuje nějaký uzel / e F a X je dosažitelná z nějakého počátečního stavu SO e Srn- □ Všimněme si, že (při značení jako ve výše uvedeném důkazu) k ověření, zda L(A, F) ^ 0, stačí (i) analyzovat maximální silně souvislé komponenty orientovaného grafu G a = (S, E), což lze provést v lineárním čase vzhledem k velikosti grafu (tj. card(S) + card(E)) a (ii) ověřit dosažitelnost, což lze opět provést v lineárním čase. Označíme-li n = card(S), pak problém L(A, F) ^ 0 ? je rozhodnutelný, a to v čase 0(n2). Poznámka 1.15. Bez důkazu uveďme, že problém neprázdnosti pro Bůchiho automaty (L(A, F) 0?) je logspace úplný pro NLOGSPACE a že problém neuniversality pro Bůchiho automaty (L(A, F) ^ Z1"?) je logspace úplný pro PSPACE. I když uzavřenost Búchi-rozpoznatelných jazyků vůči operaci doplňku dokážeme až v následující části 1.5, v zájmu úplnosti námi uváděných výsledků o rozhodnutelných problémech zde zmiňme ještě tyto výsledky: Důsledek 1.16. Problém inkluse a ekvivalence je pro Bůchiho automaty rozhodnutelný. Důkaz. Z uzavřenosti na průnik a komplement (doplněk, zde pro jazyk L značený jako ^L) okamžitě plyne, že oba tyto problémy lze redukovat na problém prázdnosti, protože Lx C L2 ^=> Li n ^L2 = 0. □ 1.5 Komplementace Bůchiho automatů a relace kongruence Jak již bylo naznačeno v poznámce 1.10 je důkaz uzavřenosti Búchi-rozpoznatelných jazyků na komplement netriviální. V literatuře se lze setkat s několika přístupy - zde se budeme držet (do jisté míry) původního Bůchiho důkazu; některé ostatní techniky budou naznačeny v dalším textu. Nejprve nastiňme základní myšlenky Bůchiho důkazu: pro daný automat A = (S, S, A, S, definujeme kongruenci ~A nad S* tak, že dvě (konečná) slova u, v prohlásíme za ekviva-letní, jestliže pro každé p,q e S platí p ^> q ^=^> pA^a navíc při uvedené posloupnosti přechodů pro u lze projít stavem z F, když a jen když je toto možné i pro uvedenou posloupnost přechodů při čtení slova v. Snadno se nahlédne, že ~A je kongruence a má pouze konečně mnoho tříd rozkladu (konečný index). Označíme-li symbolem [u] třídu rozkladu obsahující slovo u, ukáže se, že libovolný w-jazyk tvaru [w].[t>]" je buď celý obsažen v L(A), nebo je s ním disjunktní. Dále lze ukázat1, že každé w-slovo lze zapsat jako posloupnost uqUi ... konečných slov takových, že všechna Ui, í > 1, patří do stejné ^-třídy. Aplikací tohoto výsledku na w-slova nepatřící do L(A) se nahlédne, že Eu — L(A) je reprezentovatelná jako sjednocení množin [w].[t>]", kde u, v jsou taková, že w.t>" ^ L(A). Navíc se jedná o sjednocení 1. původní Bůchiho důkaz aplikací Ramsey-ovy věty pro spočetné množiny, zde pomocí lemmatu 1.17 1.5. KOMPLEMENTACE BÚCHIHO AUTOMATŮ A RELACE KONGRUENCE 13 konečně mnoha takových množin (rozklad podle ~, má pouze konečně mnoho tříd) a lze jej snadno reprezentovat jako Bíichiho automat. Lemma 1.17. Nechi ~ je libovolná kongruence na S* s konečným indexem. Pak pro libovolné uj-slovo a e Eu existují'~—třídy U, V takové, že a E U.V1^ (navíc lze předpokládat, že V.V C V). Důkaz. Nechť ~ je libovolná kongruence na S* konečného indexu. Pro dané a e Eu řekneme, že jeho dvě pozice k, k' se spojují na pozici m, pro m > ma,x{k, k'}, jestliže platí a[k,m) ~ a[k',m). V takovém případě píšeme k =™ či stručněji k =a k', jestliže platí k =™ fc' pro nějaké m. Poznamenejme, že platí-li k =™ pak pro každé to' > to platí i k =™ k', protože a[k,m) ~ a[/j',m) implikuje m)a[m, to') ~ a[k',m)a[m,m'). Dále si všimněme, že =Q je relací ekvivalence s konečným indexem, protože je definována pomocí kongruence ~, která má konečný index. Pak tedy existuje nekonečná rostoucí posloupnost pozic ko, ki,..., které všechny patří do stejné =a-tíídy. Můžeme předpokládat, že k0 > 0 a že pro všechna i > 0 úseky a[k0, ki) patří do stejné ~-rřídy, označme ji V (v opačném případě uvážíme vybranou nekonečnou podposloupnost, aby tyto předpoklady byly splněny). Konečně označme U tu ~-třídu, která obsahuje a[0, ko). Při tomto značení pak platí: 3k0.(k0>0 A a[0,k0) G U A A Vz > 0.( 3ki.( ki > ki-i A a[k0,ki) G V A k0 = a h ))) . Ukážeme, že a e U.VU. Předpokládejme tedy, že máme ko a nekonečnou posloupnost &i, &2,... splňující (1.2). Přechodem k vhodné podposloupnosti lze dále předpokládat, že pro všechna i > 0 se pozice ko, ki spojují na nějaké pozici to takové, že to < ki+i, a tedy se spojují i na pozici ki+1. Nyní ukážeme, že a[ki, ki+1) e V pro všechna i > 0. Z (1.2) okamžitě máme a[ko, ki) e V. Pro z > 0 z (1.2) máme o:[fco, £ víme, že pozice ko, ki se spojují na pozici fcj+i. Odtud plyne, že o:[fcj, fcj+i) G y, a tedy a e t/. V". Nyní zbývá ukázat tvrzení V.V C y. Jelikož y je třída rozkladu podle kongruence, pak stačí ukázat, že V.V D V ^ 0. Toto však platí, protože úseky a[k0, ki), a[ki, ki+1) a a[ko, ki+i) patří do V pro libovolné z > 0. □ Saturace. Mějme libovolnou kongruenci ~ na £*. Řekneme, že ~ saturuje w-jazyk L C S*, jestliže pro všechny ~-rřídy U, V platí: vu,v e s*/^ : t/.v" n l ^ 0 =^> t/.y" c l . Značení. Pro daný Bůchiho automat A = (S, S, A, Sin, F) píšeme s s', právě když existuje běh automatu A na slově w ze stavu s do stavu s' takový, že alespoň jeden ze stavů tohoto běhu (včetně stavů s a s') patří do F (srv. se značením s —> s'). Mimo značení Wss, = {w G S* I s 4 s'} , zavedené již v úvodu části 1.4, budeme používat ještě toto značení: 14 KAPITOLA 1. BŮCHIHO AUTOMATY Zřejmě i Wfs, je regulární (dokažte!). Kongruence ^A. Pro daný Bíichiho automat A = (S, S, A, 5in, F) definujme relaci ekvivalence ~A na S* takto: !i~ji)ÄVs,s'e5.((s4s' ^=^> s A s') A (s-p^s' ^=^> s^s')), což lze ekvivaletně zapsat, kde [w] značí tu třídu rozkladu Y>* / ^A obsahující slovo w, jako: N = ns,S'£5 {w*s> I ™ e WW} n O..,-. . {Wfs, Iwew&yn fl.,-. . {£*-Wflfl, |^WW}n a.- . {>:• "Z- .•/u/;.!. Tedy každá ^-třída obsahující slovo w je průnikem všech takových regulárních množin WSS', WgS,, S* - WSS' a S* - Wfs,, které obsahují slovo w. Tedy z regularity každé Wss/ a Wfs, plyne, že každá ^-třída [w] je regulární. Díky konečnosti množiny stavů S má ~A konečný index a lze ukázat (dokažte!), že ~, je kongruence. Ukažme nyní, že L(A) lze. reprezentovat pomocí tříd (pro jisté technické zjednodušení a bez újmy na obecnosti uvažujeme automat s jediným počátečním stavem). Lemma 1.18. Nechi A je Búchiho automat nad S. Pak ^A saturuje uj-jazyk L(A). Důkaz. Nechf A= (S, S, A, {qo}, F) je Búchiho automat. Mějme w-slovo a = uviV2 ■ ■ ■ z jazyka L(A) a ^-třídy U, V takové, že u G U a Vi G V, i > 1. Ukážeme, že pak U.V" C L(A). Uvažme akceptující běh automatu A na slově a. V tomto běhu tedy existují stavy si, S2, ■ ■ ■ takové, že Qo si -4 s2 -4 s3 -4 • • • , kde navíc platí Si Sj+i pro nekonečně mnoho i > 1 . Mějme nyní f3 libovolné takové, že f3 G t/.V". Zřejmě stačí ukázat, že f3 G L (.4). Slovo /? lze psát ve tvaru f3 = u'v^v^ ■ .., kde v! G t/, ^ G V, z > 1. Dle předpokladu lemmatu jsou U, V ~,-třídy, a tedy u ^A v!, Ví ^A v[, takže obdržíme u' v' v'„ v'„ qo ->• si -4 s2 -4 s3 -4 • • • , kde navíc platí si si+i Pro nekonečně mnoho z > 1 . Takže jsme získali běh automatu A na slově /?, kde se nějaký stav z F vyskytuje nekonečně častokrát, a tedy j3 G L(A). □ Věta 1.19. Nechi L C S" je Bůchi-rozpoznatelný jazyk, pak S" — L je též Búchi-rozpoznatelný. Je-li dán Búchiho automat rozpoznávající L, pak lze zkonstruovat Búchiho automat rozpoznávající— L. 1.5. KOMPLEMENTACE B ÚCHIHO AUTOMATŮ A RELACE KONGRUENCE 15 Důkaz. Spojením Lemmat 1.17 a 1.18 získáváme Jelikož dle předpokladu má ^A konečný index a všechny ^-třídy jsou regulární, je L w-regulární j azyk. Díky Lemmatu 1.17 a vztahu (1.3) dále získáváme a tedy — L je také w-regulární a tudíž Bíichi-rozpoznatelný. Poznamenejme, že prázdnost průniku U.VU O L je rozhodnutelná (viz Věta 1.9 -uzavřenost na zřetězení a w-iteraci, Věta 1.8 - uzavřenost na průnik a Věta 1.14 - rozhod-nutelnost prázdnosti). Užitím Věty 1.12 můžeme tudíž zkonstruovat Búchiho automat A Výše uvedené Lemma 1.18 lze použít též k formulaci w-jazyků pomocí konečných pologrup. Zopakujme, že jazyk W C S* je regulární, právě když existuje konečný monoid (pologrupa s jedničkou) M a monoidový homomorfismus / : S* —>• M takový, že W je sjednocením (jistých) množin /_1(m), kde m e M. Jelikož je pro libovolný Búchiho automat A konečným monoidem, dostaneme s použitím Věty 1.12 a Lemmatu 1.18 toto tvrzení: Věta 1.20. Jazyk L C Eu je uj-regulámí, pravé když existuje konečný monoid a monoidový homomorňsmus f : S* —>• M takový, že L je sjednocením jistých množin /_1(m).(/_1(e))", kde m, e e M (a kde lze předpokládat, žee.e = e). Pro případ jazyků konečných slov rovněž připomeňme tzv. prefixovou ekvivalenci ^L , která je definována takto: Nechf L C S* je libovolný (ne nutně regulární) jazyk. Na S* definujeme relaci ^L zvanou prefixová ekvivalence pro L takto: pro u, v e S* klademe Lze ukázat, že ^L je pravou kongruencí, a to největší takovou, která saturuje L (tj. L lze vyjádřit jako sjednocení některých tříd rozkladu určeného jistou pravou kongruencí na £*, přičemž těchto tříd však obecně nemusí být konečně mnoho). V případě regulárních jazyků pak platí (viz Nerodova-Myhillova věta), že L je regulární, právě když ^L má konečný index (přičemž S*/^L, zvaná též syntaktický monoid, odpovídala minimálnímu automatu pro L - počet stavů libovolného minimálního automatu rozpoznávajícího jazyk L je roven indexu prefixové ekvivalence Pro jazyky nekonečných slov lze analogicky definovat na S* prefixovou ekvivalenci ^L takto: pro u, v e S* klademe (1.3) takový, že L(A) = Ľ" — L. □ která je opět pravou kongruencí a dále -L 16 KAPITOLA 1. BŮCHIHO AUTOMATY u ~L v <í=> Vx, y, z G S* : ((xuyz^ G L <í=> xvyz" G L)A (x(yuz)UJ G L ^=4> x(yvz)u G L)) , o které lze ukázat, že je kongruencí na S* (slova m, f jsou ekvivaletní, právě když je pomocí jazyka L nelze rozlišit jako odpovídající si úseky w-slov s nekonečným periodickým rozvojem). Celkem snadno se nahlédne, že w-regularita L implikuje, že ^L i ~L mají konečný index (analogicky j ako pro konečná slova: pro libovolný Bůchiho automat A rozpoznávající L má ~A konečný index a je zjemněním ekvivalencí ^L i ~L ). Všimněme si však, že obrácená implikace obecně neplatí: Poznámka 1.21. Existují neregulární w-jazyky takové, že ^L i ~L mají konečný index. Důkaz. Pro libovolné dané f3 G Eu nechť L(/3) je jazyk všech w-slov, která mají stejnou příponu jako /?. Pak dvě slova u, v jsou ekvivaletní, protože příslušnost w-slov ua, vol do jazyka L(f3) vůbec na u, v nezávisí, a tedy ^l(/3) má pouze jednu třídu rozkladu. Zvolíme-li f3 takové, že nemá nekonečný periodický rozvoj, pak zřejmě L(f3) není regulární (viz věta 1.14). Dále lze ukázat, že v tomto případě i kongruence —l(i3) má jen jednu třídu rozkladu. □ Konečně bez důkazu jen zmiňme, že platí "maximalita" kongruence ~L, to jest, že jazyk L je w-regulární, právě když ~L má konečný index a saturuje L; navíc ~L je nej větší kongruencí saturující L. Tento výsledek nás opravňuje nazvat S*/~L syntaktickým monoidem, kde součinem je zřetězení tříd uvedeného rozkladu. 1.6 Modifikace Buchiho akceptační podmínky V některých aplikacích, které jsou však mimo rozsah tohoto textu (například vztah Bůchiho automatů a jistých temporálních logik), je výhodnější pracovat s jistými modifikacemi Bůchiho akceptační podmínky. Uveďme alespoň jednu z nich. Zobecněný Buchiho automat je w-automat A = {A,Q), kde A = (S,^, 5j„) je LTS nad £ a Q = {Gi,..., G& | Gj C S}. Vstupní w-slovo a je akceptováno, právě když existuje běh p na a takový, že platí: Vz.l < i < k : inf (p) n Gi ^ 0. Bůchiho automat je tedy speciálním případem zobecněného Bůchiho automatu. Snadno se nahlédne, že díky uzavřenosti (deterministických i nedeterministických) Bůchiho automatů vzhledem k operaci průniku se třída akceptovaných jazyků nezmění. Při značení jako výše totiž platí: fe L(A,G) = f) L(A,Gi) . i=i Bůchiho automat A' simulující automat A = (A, Q) lze zkonstruovat takto: položíme A' = (S', £,->', Sin', F), kde S' = Sx {í,...,k}, Sin = Sin X {1} a 1.6. MODIFIKACEBŮCHIHO AKCEPTAČNÍPODMÍNKY 17 F = Gi x {1} a —/ je definována takto: (s,j) A' (t,j) je-li s A ŕ, s £ G j (s, j) A (í, z) je-li s A í, s e G j a kde z = (j mod k) + 1 . Ve druhé komponentě stavů je uchováván index j e [1, k], dokud se neprojde nějakým stavem z G j. V tom případě je pak j zvýšeno o 1 (modulo k). Aby některý ze stavů z F byl navštěvován nekonečně často, musí být nějaký stav z každé množiny Gj navštěvován nekonečně často. Obráceně, je-li možné navštívit každou z G i nekonečně často, je možné to provádět v pořadí Gi, G2, ■ ■ ■, G&, a tedy projít některým stavem z F nekonečně často. KAPITOLA 1. BŮCHIHO AUTOMATY Kapitola 2 Silnější akceptační podmínky Jak bylo ukázáno v předchozí kapitole, deterministické Biichiho automaty nerozpoznávají celou třídu w-regulárních jazyků (důsledek 1.7). Pro konstrukci komplementárního automatu tedy nešlo použít deterministický automat. Při použití nedeterministických Bůchiho automatů by záměna akceptuj ich a neakceptuj ích stavů ke komplementárnímu automatu nevedla - viz též poznámka 1.10. Zavedeme tedy silnější akceptační podmínky, které, jak uvidíme, umožní definovat deterministické automaty rozponávající celou třídu w-regulár-ních jazyků. 2.1 Mullerovy automaty Jednou z možností, j ak obejít výše naznačené problémy, je specifikovat akceptační podmínku tak, aby "akceptační cyklus" v automatu obsahoval pouze samé akceptující stavy; je zřejmé, že takto musíme specifikovat všechny akceptační cykly. Následující definici zavedl Muller. Mullerův automat. Nechť A = (S, A, Sin) je konečně stavový LTS nad S. Řekneme, že w-automat A = (A, Acc) je Mullerův automat, právě když Acc je tzv. Mullerova akceptační podmínka (MAC): je dána množina F C 2S podmnožin množiny stavů S, F = {Fi, F2,..., Fk \ Fi C S}, zvaná Mullerova akceptační tabulka. Slovo a : No —>• S je akceptováno, právě když existuje běh p : No —>• S na slově a takový, že inf (p) e T, tj. inf (p) = Fi pro nějaké í E {1,2,..., k}. Tuto podmínku (A akceptuje a) můžeme formálně zapsat takto: (MAC) 3p.(p(0) G Sm A \/i.{p{i) ^ p(í + 1) G A) A inf (p) G J") Uvedený Mullerův automat A značíme (A, F) nebo též (S, S, A, Sin, F). Jazyk rozpoznávaný (též akceptovaný) Mullerovým automatem A = (A, F) je množina L(A) = {a e S" i A akceptuje a} všech cj-slov akceptovaných tímto automatem a značíme jej též L (A, F). 19 20 KAPITOLA 2. SILNĚJŠÍ AKCEPTAČNÍPODMÍNKY Mullerova akceptační podmínka vskutku klade přísnější požavky na úspěšný běh, než podmínka Búchiho: každá množina (položka Mullerovy tabulky) F e T klade positivní požadavek na stavy z F (všechny musí být navštěvovány nekonečně mnohokrát) a současně negativní požadavek na stavy z S — F (tyto musí být navštíveny jen konečně mnohokrát). Jinak řečeno, každý úspěšný běh musí od jisté pozice procházet jen přes stavy z F, a to bez přechodu do jakéhokoliv stavu mimo F. Formálně lze podmínku inf (p) e T z MAC zapsat jako formuli 1. řádu takto: v ( a vi J ' > { '■ pW = q a a 3 > i'■ p(j) = i) Fer qeF qeS-F Příklad 2.1. Připomeňme Búchiho automat A\ z příkladu 1.4, který akceptoval jazyk L C {a, ď}" všech slov takových, která obsahovala nekonečně mnoho výskytů symbolu a. Ai = ({si, s2}, {», b}, Ai, {si}, {si}) je deterministický automat s totálnípřechodovou funkcí a s Búchiho akceptační podmínkou {si}. Navrhnout Mullerův automat A akceptující tentýž L je snadné: daný LTS se vůbec nezmění (tj. zůstává deterministický) a MAC je T = {{si}, {si, s2}}. Dále jsme ukázali, že doplněk jazyka L není aceptován žádným deterministickým Búchiho automatem. Snadno se ověří, že doplněk jazyka L akceptuje týž Mullerův automat (tedy s týmž deterministickým LTS), který akceptoval L s tím, že akceptační podmínka se změní na {{s2}}. Je tedy vidět, že deterministické Mullerovy automaty akceptují ostře větší třídu jazyků, než deterministické Búchiho automaty. □ Simulace Lemma 2.2. Ke každému Búchiho automatu existuje ekvivaletníMullerův automat. Důkaz. V tvrzení lemmatu obsažená simulace Búchiho automatu automatem Mullerovým je přímočará: v Mullerově akceptační tabulce zřídíme položku pro každou podmnožinu stavů, která obsahuje akceptující stav daného, simulovaného Búchiho automatu. Nechf (A, G), kde A = (S,^, Sin) je Búchiho automat nad S. Simulující Mullerův automat je (A, Tg), kde TG = {F C S \ F n G ^ 0}. Snadno se nahlédne, že L(A, G) = L(A, Tq)'- libovolný úspěšný běh Búchiho automatu bude vyhovovat jedné z položek v Mullerově akceptační tabulce Tq- Obráceně, jakýkoli běh vyhovující některé položce z Tg musí projít některým stavem z G nekonečně mnohokrát. □ Z výše uvedené konstrukce je vidět, že simulující (A, Tg) je deterministický, právě když simulovaný (A, G) je deterministický (výchozí LTS A se nezměnil - tato simulace tedy ani nezavádí, ani neodstraňuje nedeterminismus). Lemma 2.3. Ke každému Mullerovu automatu existuje ekvivaletní Búchiho automat. Důkaz. Ukážeme, že libovolný Mullerův automat lze simulovat nedeterministickým Búchiho automatem. Nechf (A, T) je Mullerův automat, kde T = F2,..., F^.}. Nejprve pro každé i, i = 1,..., k, zkonstruujeme Búchiho automat A% = (Ai, G i) takový, že A% akceptuje vstup a, právě když existuje běh p automatu (A, T) na a s vlastností inf (p) = Fj. 2.1. MULLEROVY AUTOMATY 21 Při simulaci běhu automatu (A, F) na slově a simulující Ai nedeterministicky uhodne, že již nebudou navštíveny žádné stavy z S — Ff, následně tedy musí kontrolovat korektnost své volby: simuluje (či přesněji: je schopen simulovat) pouze ty přechody, které "nevybočí" mimo Fi. Současně Ai musí při cyklení přes množinu stavů Fi kontrolovat, zda jsou vskutku všechny stavy z Fi navštěvovány nekonečně častokrát. Nechť A = (S, ->•, Sin) a Ft = {sn ,sÍ2,..., slm}. Konstruujeme At = (A^Gj), kde Ai = (Si, —>j, Sln) a Gj jsou definovány takto: • 5i = 5u{(a,cyklusi,j) |aeFi,je{0,l,...,m-l}}, • relace přechodu —>-j je definována takto (upozorněme, že ve třetím a čtvrtém řádku definice přechodové relace —>-j je index j + í u stavu počítán modulo to): s —>i s je-li s —> s s Aj (s^cykluSj, 0) je-li s A s1, s' e Ft (s, cyklus^ j) \ (a'.cykluSi, j) je-li s A s', s' e Fi} s' sij+1 (s,cyk\uSi,j) \ (s'^ykluSj, (j + l)modm) je-li s A s', s' e Fi, s' = slj+1 • Slin = Sin • Gi = {{sim,cyk\uSi,m-ľ)} Hledaný Bůchiho automat simulující daný automat Mullerův je zřejmě sjednocením všech právě zkonstruovaných Ai = (Ai, G i),i = 1,..., k -jeho existence i konstrukce je dána větou 1.8 o uzavřenosti Bůchi-rozpoznatelných jazyků vůči sjednocení. Snadno se nahlédne, že L(A, F) = \J°=1 L(Al,Gl). □ Z právě uvedených lemmat plyne, že třída w-jazyků rozpoznatelných Mullerovými automaty je totožná s třídou Bůchi-rozpoznatelných (tj. w-regulárních) jazyků. Příklad 2.1 klade přirozenou otázku, zda deterministické Mullerovy automaty rozpoznávají celou třídu w-regulárních jazyků; velmi netriviální důkaz, že tomu tak je, podal McNaughton. Větu, která nese jeho jméno, uvádíme bez důkazu. Věta 2.4. (McNaughton). Každý u-regulární jazyk je rozpoznatelný nějakým deterministickým Mullerovým automatem. Povšimněme si, že McNaughtonova věta spolu s oběma simulacemi uvedenými v lemmatech 2.2 a 2.3 podává (alternativní) konstrukci komplementárního automatu pro daný Bůchiho automat. Důvod je v tom, že k danému (nyní bez újmy na obecnosti) deterministickému Mullerovu automatu (A, F) s totální přechodovou funkcí lze komplementární (doplněk rozpoznávající) automat zkonstruovat velmi snadno: v (MAC) namísto F stačí položit F = 25-J". Získáme tedy Mullerův automat (A, j"), kde F = {F C S \ F £ F}. Snadno se nahlédne, že L(A, F) = E" - L(A, F). Klíčovým a nejtěžším místem zůstává převod (obecně) nedeterministického Bůchiho automatu na nějaký (ne nutně Mullerův) deterministický w-automat takový, že deterministické w-automaty tohoto typu rozpoznávají všechny w-regulární jazyky. 22 KAPITOLA 2. SILNĚJŠÍ AKCEPTAČNÍPODMÍNKY 2.2 Rabínovy a Streettovy automaty Důkaz McNaughtonovy věty bývá v dnešní době podáván nepřímo pomocí tzv. Safrovy konstrukce, která převádí libovolný nedeterministický Búchiho automat na deterministický w-automat s tzv. Rabínovou akceptační podmínkou - o těchto automatech pojednává bezprostředně následující sekce. 2.2.1 Rabínův automat Níže uvedenou akceptační podmínku pomocí tzv. tabulky dvojic (anglicky "pairs table") zavedl poprvé Rabin. Rabínův automat. Nechf A = (S, A, Sin) je konečně stavový ĽTS nad S. Řekneme, že w-automat A = (A, Acc) je Rabínův automat, právě když Accje tzv. Rabínova akceptační podmínka (RAC): je dána množina VT C 2S x 2S dvojic podmnožin množiny stavů S (značená VT = {(Gi, i?i), (G*2, R2), ■ ■ ■, (Gk,Rk)} a zvaná též Rabínova tabulka). Slovo a : No —>• X je akceptováno, právě když existuje běh p : No —>• S na slově a takový, že 3i.í < í < k : inf (p) n Gz 7^ 0 A inf(p) n Rz = 0. Tuto podmínku (A akceptuje a) můžeme formálně zapsat takto: (RAC) 3P-(P(°) e Sin A Vi.(p(i) ^ p(i + 1) G A) A 3i. 1 < i < k : inf (p) n G, ^ 0 A inf (p) n i?4 = 0) Uvedený Rabínův automat A značíme (A, VT) nebo též (S, S, A, Sin, VT). Jazyk rozpoznávaný (též akceptovaný) Rabínovým automatem A = (A, VT) je množina L(A) = {a e S" I A akceptuje a} všech cj-slov akceptovaných tímto automatem a značíme jej též L (A, VT). Každá dvojice (Gí,Rí) v tabulce dvojic Rabínova automatu tedy specifikuje (podobně jako v Mullerově automatu) positivní a negativní požadavky kladené na úspěšný běh. Positivní podmínka kladená na stavy z Gi je totožná s Búchiho podmínkou. Negativní podmínka kladená na stavy z Ri odpovídá podmínce pro konečně mnoho výskytů stavů z S — Fi, uvažuj eme-li v Mullerově akceptační tabulce položku Fj. (Pokud si představíme Gi a Ri jako zelená resp. červená světla typu i, pak běh p splňuje (Gi, Ri), jestliže některé zelené světlo typu i (tj. z G i) bliká nekonečně častokrát a současně červené světlo typu i (tj. z Ri) zablikalo jen konečně mnohokrát.) Podmínku 3r. 1 < r < k : inf (p) n Gr ^ 0 A inf (p) n Rr = 0 z RAC lze zapsat jako formuli l.řádu takto: v (v vi j >{'■ p(fi = q a a > *: ^0') = 1) re{l,...,k} q£Gr qeRr Příklad 2.5. Vrátíme-li se opět k příkladu 1.4, pak L(Ai) (nekonečně mnoho výskytů 'a') je akceptován Rabínovým automatem, který má LTS jako A\, s tabulkou obsahující jedinou dvojici ({si}, 0). Doplněk L(A\) je akceptován Rabínovým automatem, který má opět tentýž LTS a jeho tabulka obsahuje jedinou dvojici ({s2}, {si})- 2.2. RABÍNOVY A STREETTOVY AUTOMATY 23 Simulace Btichiho automaty lze jednoduše simulovat pomocí Rabínových automatů: je-li (A, F) Búchiho automat, pak ekvivaletní Rabínův automat je (A, VTf), kde VTf = {{F, 0}}. Tedy Bůchiho automat je speciálním případem Rabínova automatu - stačí totiž položit k = 1, d = F, i?i = 0. V obráceném směru můžeme každý Rabínův automat simulovat Bůchiho automatem pomocí konstrukce, která je podobná té, jež byla užita při simulaci Mullerova automatu Búchiho automatem (viz lemma 2.3). Opět stačí, díky uzavřenosti Búchiho automatů vůči sjednocení, zkonstruovat pro každou položku (Ri, G i) G VT jeden ("izolovaný") Bůchiho automat (Ai, Fi). Každý (Ai, Fi) opět nedeterministicky uhodne, kdy se již žádný ze stavů z Ri neobjeví a následně toto kontroluje spolu s tím, že alespoň jeden ze stavů z Gi se objevuje v běhu nekonečně mnohokrát. Nastíněnou konstrukci nyní popišme formálně. Nechf A = (S, Sin) a VT = {(Gi, (G2, R2),(Gk,Rk)}. Konstruujeme Ai = (Ai, Fi), kde Ai = (Si, —>j, Slin) a Gi jsou definovány takto: • Si = S u {(s, cyklus,, j) \ seS-Ri, je {0,1}}, • relace přechodu —>-j je definována takto: a s \ (s', cyklus,, 0) je-li s -í je-li s -í (s,cyklus,, 0) A, (s',cyklus,, 0) je-li s A (s,cyklus,, 0) A, (s1,cyklus,, 1) je-li s A s (s,cyklus,, 1) A, (s1,cyklus,, 0) je-li s A s • Slin = Sin • Fi = {(s,cyklus,, 1) \ seS-Ri} Poznámka 2.6. Dále si všimněme, že libovolný Rabínův automat je speciálním případem automatu Mullerova - každá dvojice (Gi, Ri) G VT generuje "částečnou" Mullerovu ta- Ri Ri, s> i G, Ri, s' G Gi Ri bulku Ti = {F C S i F n G, + 0, F n R, T = Ui£{i ... fej J^, což lze zapsat stručněji jako k T={FCS\ \J(FnGiŕ 0} a hledaná Mullerova tabulka je A FDRl = 0)} Jelikož jsme LTS nijak nemodifikovali, platí, že simulující automat je deterministický, právě když simulovaný automat je deterministický. Konečně poznamenejme, že pro simulaci Mullerova automatu automatem Rabínovým je nutné použít konstrukci, která je analogická konstrukci použité při simulaci Mullerova automatu Búchiho automatem. Tato konstrukce vnáší nedeterminismus. Není známa nějaká přímočará konstrukce, která by byla simulací deterministického Mullerova automatu deterministickým Rabínovým automatem. Nicméně zdůrazněme (opět s odkazem na Safra-ovu konstrukci a Poznámku 2.6), že deterministické Rabínovy automaty rozpoznávají celou třídu w-regulárních jazyků. 24 KAPITOLA 2. SILNĚJŠÍ AKCEPTAČNÍPODMÍNKY 2.2.2 Streettův automat Níže uvedenou akceptační podmínku, definovanou opět pomocí tabulky dvojic, zavedl poprvé Streett (1988). Při nekonečných výpočtech jsou tyto automaty vhodné pro specifikaci tzv. "fairness" podmínek, jako je například podmínka typu "požaduje-li proces přidělení zdroje nekonečně častokrát, pak systém garantuje splnění tohoto požadavku rovněž nekonečně častokrát". Streettův automat. Streettův automat je w-automat definovaný jako dvojice (A,VT), kde A = (S, A, Sm) a VT = {(d, (G2, R2),(Gk,Rk)} jsou definovány tak, jako u Rabínova automatu. Streettova akceptační podmínka (SAC) je definována takto: Slovo a : No —>• X je akceptováno, právě když existuje běh p : No —>• S na slově a takový, že VO inf(p) n Rt ^ 0. Tuto podmínku můžeme formálně zapsat takto: (SAC) 3M0) G Sin A ^ p{-1 + l) G A) A Ví. 1 < i < k : inf (p) C\Gl^% =^ inf (p) C\Rl^$) Uvedený Streettův automat A (opět) značíme (A,VT) nebo též (S, S, A, Sin, VT). Je tedy vždy nutno uvést, zda se jedná o interpretaci VT jako tabulky Rabínovy, či Street-tovy, pokud to není zřejmé z kontextu. Pokud nebude tato interpretace zadána, budeme o (A, VT) mluvit jako o automatu s tabulkou dvojic. Všimněme si, že definice SAC přímo koresponduje uvedenému typu fairness podmínek: jestliže je některý ze stavů z Gr navštěvován nekonečně mnohokrát, pak musí v Rr existovat nějaký stav, který je navštěvován rovněž nekonečně mnohokrát a splnění této podmínky je požadováno pro všechna r, 1 < r < k. Podmínku Vr. 1 < r < k : inf (p) nGr=/M inf (p) n Rr ^ 0 ze SAC lze zapsat jako formuli 1. řádu takto: a v vi j >{'■ pW = q v v vi j >{'■ p(fi = q^ ■ r£{l,...,k} q£Gr qeRr Přímo z definice Streettova automatu se vidí jeho vztah k automatu Rabínovu: Tvrzení 2.7. Nechi A = (A, VT) je automat s tabulkou dvojic. Nechi LR = L(A, VT), kde VT je interpretována jako Rabínova akceptační podmínka, a L$ = L(A,VT), kde VT je interpretována jako Streettova akceptační podmínka. Pak L s je doplňkem Lr. Simulace Každý Bůchiho automat (S, S, —>•, 5j„, F) je opět specálním případem Streettova automatu - stačí položit k = 1, Gi = S, i?i = F bez změny LTS (tj. PTF = {(S, F)} pro Street-tovu interpretaci). O konstrukci Bůchiho automatu simulujícího libovolný daný Streettův automat pojednává následující lemma (M.Vardi). Lemma 2.8. Nechi A = (A, VT) je Streettův automat nad S, kde A = (S, ->•, Sm), VT = {(Gi, i?i), (G2, i?2), • • •, (Gfe, Rk)} an = card(S). Pak lze zkonstruovat Bůchiho automat A' = (S', S, , S'm, F) takový, ze L (A) = L (A)' a card(S') = n ■ 20(-k\ 2.2. RABÍNOVY A STREETTOVY AUTOMATY 25 Důkaz. Jako obvykle A', který simuluje automat A, hádá pozici v běhu p takovou, že každý stav navštívený za touto pozicí bude de facto navštíven nekonečně častokrát; od této pozice dál musí A' kontrolovat splnění akceptační podmínky pro každou dvojici (Gi, Ri) G VT■ Automat A' tedy musí za uvedenou pozicí kontrolovat pro každé i implikaci: jestliže se některý ze stavů z Gi vyskytuje nekonečně častokrát, pak i některý ze stavů z Ri se vyskytuje nekonečně častokrát. Toto lze realizovat tak, že A' udržuje, jako komponenty svého stavu, dvě množiny: v první z nich udržuje seznam indexů i takových, že některý stav z Gi je navštěvován nekonečně častokrát, kdežto ve druhé z nich seznam indexů navštěvovaných stavů z Ri. Jakmile se první množina stane podmnožinou množiny druhé, je tato druhá množina nastavena na prázdnou množinu. Je vidět, že akceptační podmínka bude splněna, právě když je zmíněná druhá množina nastavena na prázdnou množinu nekonečně častokrát. Formálně lze naznačenou konstrukci simulujícího automatu A' = (S', S, —/, S'in, F) zapsat takto: • Si = SU{(s,X,Y) \seS, X,Y C{l,2,...,k}}, • relace přechodu —/ je definována takto: s 4' s< je-li a s —> s' 1 s A' (*',( m) je-li a s —> (s,X,Y) A' (s',XUG,YUR) je-li a s —> X U G % Y U R, kde G = i s' e Gi,l XUGCYUR, • S" — f- . F = {(s,X,