0ÖIS Off,
JÁS MK'
FI MU
Fakulta informatiky Masarykova univerzita
Automaty nad nekonečnými slovy
Mojmír Křetínský
Učební text FI MU                                                                                       verze 1.0
Copyright © 2002, FI MU
prosinec 2002
Obsah
1         Büchiho automaty   3
1.1     Jazyky nekonečných slov    3
1.2     uj-automaty   4
1.3      Uzáverové vlastnosti Büchi-rozpoznate Iných jazyků    8
1.4     Regulární uj-jazyky    10
1.5     Komplementace Büchiho automatů a relace kongruence    12
1.6     Modifikace Büchiho akceptačnípodmínky    16
2        Silnější akceptační podmínky    17
2.1     Mullerovy automaty    17
2.2     Rabínovy a Streetovy automaty   20
2.2.1  Rabínův automat   20
2.2.2   Streetův automat   22
1
2                                                                                                                    OBSAH
Kapitola 1
Büchiho automaty
1.1   Jazyky nekonečných slov
Nechť S je konečná abeceda. S * značí množinu všech slov konečné délky, typicky označovaných«, v, w,... G S*, w = a0ai... an, kde en g S. Slovo nekonečné délky, nazývané též w-slovo, definujeme jako funkci a : N0 —> S. Symbolem S" značíme množinu všech slov nekonečné délky, typicky označovaných«, ß... G S u. Tedy a(i) označuje písmeno na i-té pozici a w-slovo a můžeme a často též budeme zapisovat jako a = a(0)a(l).... Dále označme EK, = E*USW.
Pro přirozená m, n taková, zem <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, lu] = 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 3un resp. 3<un. Formálně definujeme 3wn.</>(n) jako zkratku pro Vi.3n.(n > i A </>(n)) a dále 3 <u n jako zkratku pro 3n.(p(n) A 3íij.(j > i =>• ~«f>(j)). Analogicky zápis Vwn.</)(n) budeme interpretovat j ako zkratku pro 3i.Vn.(n > i => (j>(n)).
NechťX C S*, y C S°°. Pro x G X, y G Y definujeme jejich zřetězení jako slovo x.y = x(0)x(l)... x(n)y(0)y(l)..., kde x (i) = Xj (symbol '.' často vynecháváme, tj. místo x.y píšeme stručněji xy).
Dále zřetězení jazyků X CE'aľC S°° definujeme jako jazyk
X.Y = {x.y \xeX,yeY] a nekonečnou iteraci (w-iteraci) jazyka X C S * jako jazyk
Xu = {x0xi ... | x» G X - {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, en G S a X = {«}, pak X" = {«"}, kde uu je nekonečné slovo                                            které též můžeme
zapsat jako uu ... . Pro Y = {x, y} je F" = {xx ..., xy ..., yx ..., yy ..., ...}.
3
4
KAPITOLA 1.  BUCHIHOAUTOMATY
Dále pro ICE* definujme
pref(X) = {u G S* | 3v.uv G X} lim(X) = {a G S" | 3wn.a[0, n] G X} ;
tj. a G lim (X), právě když a má nekonečně mnoho prefixů v X. Poznamenejme, že často používanou notací pro lim (X) jsou též značení X či Xó.
Operátory w-iterace a lim jsou oba typu S* —> iľw, 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 Iim(ř7) = 0.
(b)  Je-li U = {ab) + , pak lim(t/) = (a6)w.
(c)  Je-li ř7 = (a*b)+ = (a+b)*b, tj. U je množina všech slov končících symbolem b, pak li m (U) = (a* b)u je množinou všech w-slov obsahujících nekonečně mnoho výskytů b.
1.2   cj-automaty
Přechodový systém A (s návěštími a počátečními stavy), zkráceně LTS (labelled transition system) definujeme jako
A = {&, Li, A, bin).
kde S je množina stavů, S je konečná (vstupní) abeceda, ACSxSx S je přechodová relace a Si„ C 5 je množina počátečních stavů. Namísto (s, a, s') G A často píšeme s AA 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ě j ej 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 S x S do S.
Přechodový systém A nazveme deterministický, jestliže card{Sin) = 1 a přechodová relaceje funkcí A : S*xS —> S*. VpřípadědeterministickýchLTS lze bezújmy na obecnosti předpokládat, že A je totální, 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,ia2 ... am slovo nad S, pak klademe s A s', právě když existují so, si,..., sm G S* taková, že s = sq, sj_i -4 sž (0 < i < m) a sm = s'.
Běh LTS. Nechť A = (S, A, Sin) je LTS nad S, w e S*, w = a0ai ...an konečné vstupní slovo a a : N0 —> S vstupní w-slovo. Běh p systému A na slově w je konečná posloupnost s0, «i, • • • «n+i stavů z 5 taková, že Vi. 0 < i < m : sž -^ si+1. Běh p systému A na w-slově a je definován jako nekonečná posloupnost p : N0 —> S taková, že Vi .i G N0 : p (i) "-+ p(i + 1). Je-li navíc p(0) G Sin, resp. s0 G 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.  cü-AUTOMATY
5
Dále pro libovolné w-slovo p : N0 —> S klademe
inf(p) = {seS| 3wn. p(n) = s}: occ(p) = {s G S I 3n. p(n) = s}
tedy i nf (p) definujeme jako množinu symbolů z S, které se vyskytují v w-slově p nekonečně často, kdežto occ(a) je množina symbolů z S, které se v a vyskytují.
^-automat. Nechť A = (S, A, Sm) je LTS nad S, pak w-automatem nazveme systém A = (A, Acc), kde Acc je tzv. akceptační podmínka definující, kdyje 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ů).
Büchiho automat. Nechť A = (S, A, Sin) jeLTS nadS. Ř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ích (též finálních) stavů a slovo a : N0 —> S je akceptováno, právě když existuje běh p : N0 —> S na slově a takový, že inf(p) n F ^ 0. Büchiho podmínku můžeme stručněji zapsat takto:
(BAC)                        3p.(p(0) G Sm A Vi.(p(i) ^ P(i + 1)€A) A inf(p) n F =é 0
Uvedený Büchiho automat A značíme (A, F) nebo též (S, S, A, Sm,F). Jazyk rozpoznávaný (též akceptovaný) Büchiho automatem A = (A, F) je množina
L(A) = {a G S" I A akceptuje a}
všech w-slov akceptovaných tímto automatem a značíme jej též L(A, F). Konečně řekneme, že množina L C E" je rozpoznatelná ve smyslu Büchiho (či stručněji Büchi-rozpoznatelná), právě když existuje Büchiho automat A takový, že L = L (A).
Obrázek 1.1: typický úspěšný běh Büchiho automatu, s G S ,in, f G F
Poznámka 1.2. Büchiho akceptační podmínka tedy požaduje, aby se nějaká podmnožina množiny f1 vyskytovala v úspěšnémběhu p nekonečně častokrát: jelikož F je konečná, musí
6
KAPITOLA 1.  BUCHIHOAUTOMATY
existovat nějaký stav / G F, který se v p vyskytuje nekonečněkrát. Pokud si představíme přechodový graf Büchiho 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.                                                                          D
Podmínku inf(p) nF/0 (tj. WiBj.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:
V VGj.j > i : p(j) = q
qeF
Příklad 1.3. Mějme Büchiho automaty A = ({qi, <?2}, {a, b}, A, {qi}, {92}) , kde A je dána takto:
a                              b
qi —>■ <£>             <7i —>■ <7i
a                              b
qi —> qi      <£> —>■ q\ a B = ({<?i, g2}, {«, &}, A, {q1},{q2}),kde A je dána takto:
a
qi -> 92
a                              b
qi —> qi      92 —> q\
Obrázek 1.2: Automaty A (vlevo) a B (vpravo)
Automat A je deterministický a s totální přechodovou funkcí (resp. jeho přechodový systém má tyto vlastnosti), kdežto B je deterministický, ale jeho přechodová funkce je parciální (sestrojte ekvivaletní 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, 6} akceptující množinu právě všech takových slov, v nichž se symboly a a 6 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 nedeter-minismus 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ů.
Příklad 1.4. Nechťje dánBuchiho automat A\ = ({si, s2}, {a, 6}, Ai, {si}, {si}), kde Ai je dána takto:
a                          b
Si —>■ Si           Si —>■ s2
a                          b
s2 —>■ Si             s2 —>■ s2
1.2.  cü-AUTOMATY
1
a Büchiho automat Ai = ({si, s2}, {a,b}, A2, {si}, {«2}), kde A2 je dána takto:
a                          6                          6
Si  —> Si           Si  —> Si           Si  —> S2
6
S2 —► S2
Obrázek 1.3: Automaty A\ (vlevo) a *42 (vpravo)
Automat A z příkladu 1.3 je ekvivalentní s výše uvedeným A\ - 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 s 1 a současně všechny přechody do si jsou pod symbolem a).
Automat A2 akceptuje množinu všech w-slov, která je komplementem L(A\). Ai je nedeterministický: uhodne místo ve vstupním slově, za nímž již nejsou žádné výskyty a - taková pozice ve slově musí existovat, neboť libovolné vstupní slovo, které má být akceptováno, má jen konečně mnoho výskytů a. Následně automat kontroluje správnost svého hádání tím, že může číst pouze symboly b - z s 2 nevede žádný a-přechod a A2 by nebyl schopen pokračovat ve čtení vstupního slova, a tedy by jej nemohl akceptovat.     D
Poznámka 1.5. Jak již bylo uvedeno, A z příkladu 1.3 a A1 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{Ä2) = {a, b}* - L(Ai). Povšimnněme si, že A\ 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\).                                           □
Veta 1.6. Jazyk L C Suje rozpoznatelný deterministickým Büchiho automatem, právě když existuje regulárni jazyk U C S* takový, že L = Iim(ř7).
Důkaz: <r=: Nechť U je regulární jazyk nad S. Pak existuje DFA A = (S, S, A, o0, F) takový, že L (A) = U. Pokud A 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 automat deterministický.
=x Nechť L je rozpoznáván deterministickým Büchiho automatem A s množinou akceptujích 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
8
KAPITOLA 1.  BUCHIHOAUTOMATY
Důsledek 1.7. Existují jazyky rozpoznatelné nedeterministickými Büchiho automaty, které nejsou rozpoznatelné žádnými deterministickými Büchiho automaty.
Důkaz: Ukážeme, že jazyk L = L(*42) z příkladu 1.4 není tvaru Iim(ř7) pro žádný regulární jazyk U. Připomeňme, že L je množinou všech w-slov nad £ = {a, b}* obsahujících nekonečně mnoho výskytů symbolu 6, ale pouze konečně mnoho výskytů symbolu a.
Sporem. Předpokládejme, že 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 G U. Odtud a z definice jazyka Ĺ plyne, že bniabu G L, a tedy opět musí existovat nějaký konečný prefix bniabn2 G U. Tedy opět z definice Ĺ plyne, že bniabn2abu G L, a tudíž musí existovat další prefix bniabn2abns G U. Tímto postupem tedy obdržíme nekonečnou posloupnost slov {bni, bniabn2,bniabn2abns,...} C U. Z definice operátoru lim plyne, že i w-slovo ß = bni abn2 abn3 a... abní • • • G Iim(ř7). Avšak ß má nekonečně mnoho výskytů symbolu a, takže jistě nepatří do L, což je ale spor s předpokladem, že L = Iim(ř7).                    D
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 Bíichi-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ů.
Veta 1.8. Jsou-li Li, L2 Q Sw Buchi-rozpoznatelnéjazyky, pak Li U L2 a Li n L2JSOU Buchi-rozpoznatelné.
Důkaz: Mějme Büchiho automaty Ai = (5i; S, Ai; S-n, Fi) takové, že Li = L(A), * = 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 Lx U L2 je rozpoznáván automatem A = (Si U S2, S, Ai U A2, S}n U Sfn, Li U L2). 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 automatu rozpoznávajího průnikje kartézským součinem stavovýchprostorů výchozíchau-tomatů a odpovídajícím způsobemj sou definovány i ostatní komponenty, například množina koncových stavuje 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
1.3.   UZÁVEROVÉ VLASTNOSTIBUCHI-ROZPOZNATELNÝCH JAZYKŮ                  9
je-li	Sl	a            1                  K	S'2	a            1                  A -► 4 G A2,	Sl^Fl
je-li	Sl	-^4 e Ai,	S2	-► si, G A2,	SlGf1!
je-li	Sl	-►«í G Ai,	S2	-► s2 G A2,	S2ÍF2
je-li	Sl	a        1             \ -^4 G Ai,	S2	a            /                  A -► s2 G A2,	s2 G F2
po přečtení a(0), a(2),..., kdežto druhý po přečtení a(l), a(3),.... Tedy za množinu akceptujících stavů průnikového automatu nelze vzít f1! 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 kopii navštěvuje své akceptující stavy. Stačí, aby každá z těchto kopií zanamenávalajen 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í Li C\L2 lze tedy definovat jako A = (S, £, A, Sin, ŕ1), kde
•  S = S1xS2x {1,2},
•  A je definována takto:
(si,s2,l) A (4,4,1)
(s!,S2,i) A (4,4,2)
(si,S2,2) A (4,4,2) (Sl,S2,2)A(4,4,l)
•   Sin = {(si, s2,1) | si G S}n, s2 G Sfn},
•  F = Sľx F2x {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ů A i. Poznamenejme, že ekvivaletně j sme mohli při konstrukci A položit F = Fľ x S2 x {í}).
Snadno se ověří, že L(A) = L(Ai) n L(A2).                                                    D
Veta 1.9. NechťU C Y** je regulární a L C E^ je Buchi-rozpoznatelný. Pak (i)      Uu je Buchi-rozpoznatelný  a (ii)     U.L je Buchi-rozpoznatelný.
Důkaz: (i) Bez újmy na obecnosti můžeme předpokládat, že U neobsahuje prázdné slovo (platí totiž, že Uw = (U - {e})w ) a že konečný automat A = (S, S, A, q0, F) rozpoznávající U má jediný počáteční stav q0, do kterého nevedou žádné přechody. Büchiho automat rozpoznávající Uu je A' = (S, S, A',q0, {%)}), kde A' = Au{s A q0 \ s A s', s' G 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 čtenáři.                                                                                                                    D
Poznámka 1.10. Uzavřenost vůči doplňku. Bůchi-rozpoznatelné jazyky j sou 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 ŕ1, a tudíž nahrazení F jeho komplementem
10
KAPITOLA 1.  BUCHIHOAUTOMATY
by způsobilo, že a by bylo opět akceptováno. Tento problém bude pro nás (mimo jiné) motivací hledat Jemnější" akceptační podmínky (viz kapitola 2).
Uzáverové vlastnosti deterministických Buchi-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).
Veta 1.11. Jsou-li Li,Li2 Q Sw deterministické Buchi-rozpoznatelné jazyky, pak i jazyky Li U L'2 a Li n L2JSOU deterministické Buchi-rozpoznatelné.
Důkaz: Mějme deterministické Bůchiho automaty Ai = (Si, £, Ai; qi,Fi) takové, že Li = L(Ai), 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 = \\m(U), tj. existují Ui C S* taková, že Li = \\m(Ui),i = 1,2. Tvrzení o existenci deterministického automatu okamžitě plyne ze vztahu Iim(ř7i U t/2) = Iim(ř7i) U Iim(ř72). Ke konstrukci odpovídajícího automatu A lze použít synchronního paralelního spojení automatů A i s množinou koncových stavů f1 = Fľ x S2U Sľ x F2. Jelikož A 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ý.                                                                                                                   D
1.4   Regulární cj-jazyky
Pro zevrubnější analýzu Bůchi-rozpoznatelnýchjazyků budeme používat toto značení: je-li dán Bůchiho automat A = (S, S, A, Sin, F), pak klademe
waa, = {w e s* IS ^ S'} .
Zřejmě každý z konečně mnoha jazyků W ss> 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
l(ä)=    U    wsos.(wssy.                 (í.i)
s0eSin,sGF
Pokud by A byl (bez újmy na obecnosti) s jediným počátečním stavem s0, pak
L(A) = l)seFWS0S.(Wssr.
Veta 1.12. Libovolný uj-jazyk L C S^ je Buchi-rozpoznatelný, právě když je konečným sjednocením množin U.VU, kde U, V C T,* jsou regulární množiny (konečných slov). Navíc lze bez újmy na obecnosti předpokládat, že V. V C V.
1.4. REGULÁRNIcu-JAZYKY
11
Důkaz: =>: platnost této implikace okamžitě plyne ze vztahu (1.1); poznamenejme, že V.V C V plyne z WSS.WSS C ^ss.
<r=: plyne z uzavřenosti Bůchi-rozpoznatelných jazyků vzhledem ke konečnému sjednocení, zřetězení a w-iteraci.                                                                                D
Reprezentaci w-jazyka ve tvaru L = Uľ=i ^í^í"' kde Ui,ViC.'Ľ*,i = l,...,n. jsou regulární výrazy, nazýváme w-regulárním výrazem.
Řekneme, že jazyk L C Su je regulární w-jazyk (či stručněji je w-regulární), právě když L = U™=1 UiV", kde t/i; Vj C S*, i = 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 Buchi-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 £ °° obsahující (i) prázdnou množinu, (ii) jednoprvkové množiny {a} pro každý symbol a G X 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 uj -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).    D
Řekneme, že w-slovo a G Ľu má nekonečný periodický rozvoj (anglicky „is ultimately periodic"), jestliže existují u, v g S* taková, že a = uvvv ....
Veta 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: nechťL = L(A, F) pro nějaký Büchiho automat (A, F). Pak a G L(A, F) je tvaru a = uviv2 ..., kde s0 ^ f a / ^ / pro všechna i > 1 a nějaká s0 G Sm, f G F. Pak i slovo ß = uv\v\... G L(A, F) a ß 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é 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, E,A, ,%„) tohoto automatu abstrahujeme od návěští hran, obdržíme orientovaný graf G a = (S, E), kde (s, s') G E <ŕ=^=> 3a G S : s —> s'. Z (1.1) zřejmě plyne, že L(A, F) =í 0, právě když y G a existuje netriviální (tj. alespoň jednu hranu obsahující) silně souvislá komponenta X taková, že (i) X obsahuje nějaký uzel f e F, a (ii) X je dosažitelná z nějakého počátečního stavu s 0 € Sin.                                        D
Všimněme si, že (pri značení jako ve výše uvedeném důkazu) k ověření, zda
12
KAPITOLA 1.  BUCHIHOAUTOMATY
L(A, F) =é 0, stačí (i) analyzovat maximální silně souvislé komponenty orientovaného grafu G a = (S, i?),cožlzeprovéstvlineárnímčasevzhledemkvelikostigrafu(tj.caríi(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ý v čase ö(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) ^ Ľul) 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
Li C L2  -^=4> Li n -.1,2 =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, H, A, Si„, F) definujeme kongruenci ~A nad H* tak, že dvě (konečná) slova u, v prohlásíme za ekvivaletní, jestliže pro každé p,q G S platí p ^ q <ŕ=> p -^ q a navíc pri 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 ~Ä 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 w-jazyk [u].[v] u je buď celý obsažen v L (A), neboje s ním disjunktní.
Dále lze ukázat1, že každé w-slovo lze zapsat jako posloupnost u 0«i ... konečných slov takových, že všechna u i, i > 1, patří do stejné ^-třídy. Aplikací tohoto výsledku na ^-slova nepatřící do L(A) se nahlédne, že Ľw —L(A)je reprezentovatelnájako sjednocení množin [u] .[v]u, kde u, «jsou taková, íeu.vu <£ L (A). Navíc sejednáo sjednocení konečně mnoha takových množin (rozklad podle ~ A má pouze konečně mnoho tříd) a lze j ej snadno reprezentovat jako Büchiho automat.
Lemma 1.17. Nechť ^ je libovolná kongruence nail* s konečným indexem. Pak pro libovolné uj-slovo a G S^ existují i-^—třídy U, V takové, že a G U.V^ (navíc lze předpokládat,
že V.V C V).
1.   původní Büchiho důkaz aplikací Ramsey-ovy věty pro spočetné množiny, zde pomocí lemmatu 1.17
7.5.  KOMPLEMENTACE BÜCHIHO AUTOMATŮ A RELACE KONGRUENCE         13
Důkaz: Nechť ~ je libovolná kongruence na S * konečného indexu. Pro dané a G Ľ u řekneme, že jeho dvě pozice k, k' se spojují na pozici m, pro m > max{fc, A;'}, jestliže platí a[k, m) ~ a[k', m). V takovém případě píšeme k =™ k', či stručněji A; =a k', jestliže platí k =™ k' pro nějaké m.
Poznamenejme, že platí-li k =™ k', pak pro každé m' > m platí i k =™ fc', protože a[k, m) ~ a[k', m) implikuje a[fc, m)a[m, m') ~ a[fc', m)a[m, m'). Dále si všimněme, že =a 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 fc0, ki,..., které všechny patří do stejné =a-třídy. Můžeme předpokládat, že fc0 > 0 a že pro všechna i > 0 úseky a[k0, h) patří do stejné ~-tří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, fc 0). Při tomto značení pak platí:
3fc0.(fco >0 A a[0,ko) e U A A Vi > 0.( 3fcj.( h > fcj_i  A a[k0,ki) G V A fc0 =a h ))) .
Ukážeme, že a G U.VU. Předpokládejme tedy, že máme fc0 a nekonečnouposloup-nostfci, fc2,... splňující (1.2). Přechodem k vhodné podposloupnosti lze dále předpokládat, že pro všechna i > 0 se pozice fc0, h spojují na nějaké pozici m takové, že m < ki+1, a tedy se spojují i na pozici ki+í. Nyní ukážeme, že a[fcj, fcj+i) G V pro všechna i > 0. Z (1.2) okamžitě máme a[k0, k\) G V. Pro i > 0 z (1.2) máme a[fco, fc») G V^ a víme, že pozice fc0,fcj se spojují na pozici fci+i. Odtud plyne, že a[fcj, fci+i) G V^atedya G U.VU.
Nyní zbývá ukázat tvrzení V.VCV. Jelikož V je třída rozkladu podle kongruence, pak stačí ukázat, že V.V n V ^ 0. Toto však platí, protože úseky a [fco, h), a[fcj, ki+í) a a [fc0, fci+i) patří do V pro libovolné i > 0.                                                                  D
Saturace. Mějme libovolnou kongruenci ~ na S *. Řekneme, že ~ saturuje w-jazyk L C S*, jestliže pro všechny ^-třídy U, V platí:
Vř7,yeS7^: U.VUC\L^<D => [/.yucL.
Značení. Pro daný Búchiho automat *4 = (S, S, A, Sm,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 as') patří do F (srv. se značením s ^ s'). Mimo značení
Wss, ={weZ*\s^s'},
zavedené již v úvodu části 1.4, budeme používat ještě toto značení:
WaFa, = {w<=X*\s^s'}.
Zřejmě i Wfs, je regulární (dokažte!).
Kongruence ~A. Pro daný Bůchiho automat A = (S, S, A, Sin, F) definujme relaci ekvivalence ~A na S* takto:
u ~A v -<=> Vs, s  G D.( (s —> s    -<=>   s^s)  A  (s -p+ s    -<=>  s-^+s)J,
14
KAPITOLA 1.  BÜCHIHO AUTOMATY
což lze ekvivaletně zapsat, kde [w] značí tu třídu rozkladu £ */~A obsahující slovo w, jako:
M    =    r\s,s'es{W.ss'\weWss,}n
ns,s,es{WsFs,\weWsFs,}n r\s,s^s{^*-Wss>\wiwaa>}n
ns,s'es{Z*-W[s,\wiWF,}.
Tedy každá ^-třída obsahující slovo w je průnikem všech takových regulárních množin Wss>, Wfs,, S* - Wss> a S* - Wfs,, které obsahují slovo w. Tedy z regularity každé Wss, a Ws^, 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. Nechť A je Büchiho automat nad S. Pak ^A saturuje uj-jazyk L (A).
Důkaz: NechrVl = (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.VU 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
U           Vi           V2           Vs
q0 —>■ si —>■ s2 —► «3 —► • • • ;
kde navíc platí
Si -^ Sj+i   pro nekonečně mnoho i > 1 .
Mějme nyní ß libovolné takové, že ß G U.VU. Zřejmě stačí ukázat, že ß G L(*4). Slovo /? lze psát ve tvaru ß = u'v'xv'2 ..., kde u' G U, v[ e V, i > 1. Dle předpokladu lemmatu jsou U, V ^-třídy, a tedy u ~A u', ví ~A v-, takže obdržíme
u            v[           v'2           v'3
q0 —>■ si —>■ s2 —► s3 —>■ • • • .
kde navíc platí
Sj -^ si+i   pro nekonečně mnoho i > 1 .
Takže jsme získali běh automatu A na slově ß, kde se nějaký stav z f1 vyskytuje nekonečně častokrát, a tedy /3 e L(i).                                                                                       D
Veta 1.19. Nechť L C Sw _/e Büchi-rozpoznateIný 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 rozpoznav ajícíYľ —L.
Důkaz:   Spojením Lemmat 1.17 a 1.18 získáváme
L =       \J      {U.VU I U.VU n L ŕ 0} .                       (1.3)
Jelikož dle předpokladu má ~A konečný index a všechny ^-třídy jsou regulární, je L ^-regulární jazyk.
7.5.  KOMPLEMENTACE BÜCHIHO AUTOMATŮ A RELACE KONGRUENCE         15
Díky Lemmatu 1.17 a vztahu (1.3) dále získáváme
Ľu - L =      \J     {U.VU l u.v" n L = 0} ,
u,veY,*/„A
a tedy Eu - L je také w-regulární a tudíž Buchi-rozpoznatelný.
Poznamenejme, že prázdnost průniku U.VU n 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 — rozhodnutelnost prázdnosti). Užitím Věty 1.12 můžeme tudíž zkonstruovat Büchiho automat Ä takový, že L(Ä) = £" - L.                                                                                  D
Výše uvedené Lemma 1.18 lze použít též k formulaci w-jazyků pomocí konečných pologrup. Zopakujme, že jazyk W C £ * je regulární, právě když existuje konečný monoid (pologrupa s jedničkou) M a monoidový homomorfismus / : £ * —> M takový, že W je sjednocením (jistých) množin /_1(m), kde m G M. Jelikož £*/=o 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 £u je uj-regulární, právě když existuje konečný monoid a monoidový homomorfismus f : £ * —> M takový, že W je sjednocením jistých množin /_1(m).(/_1(e))'*J, kde m,e G M (a kde lze předpokládat, že e.e = e).
Pro případ jazyků konečných slov rovněž připomeňme tzv. prefixovou ekvivalenci ~x, která je definována takto: Nechť L C S* je libovolný (ne nutně regulární) jazyk. Na E* definujeme relaci ~x zvanou prefixová ekvivalence pro L takto: pro u, v g £ * klademe
u ^Lv  -<=> Vw G S* : ww G L -<=> ww G L.
Lze ukázat, že ~x 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 S *, přičemž těchto tříd však obecně nemusí být konečně mnoho). V případě regulárníchjazyků pak platí (viz Nerodova-Myhillova věta), že L je regulární, právě když ~ L má konečný index (přičemž £*/~z> 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 ~x).
Prajazyky nekonečných slov lze analogicky definovat na S * prefixovou ekvivalenci ~x takto: pro u, v g £* klademe
u ^L v  -<=> V a G S^ : ua G L -<=> va G L .
která je opět pravou kongruencí a dále ~ L
u c^L v -<=> Vx, y, z G £* : {{xuyzu G L -<=> xvyzu G L)A
(x(yuz)u G L <ŕ=> x{yvzf G L)) .
o které lze ukázat, zeje kongruencí na S * (slova m, v 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).
16
KAPITOLA 1.  BUCHIHOAUTOMATY
Celkem snadno se nahlédne, že w-regularita L implikuje, že ~x i ~x mají konečný index (analogicky jako 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 ~x).
Všimněme si však, že obrácená implikace obecně neplatí:
Poznámka 1.21. Existují neregulární w-jazyky takové, že ~ x i ~x mají konečný index.
Důkaz: Pro libovolné dané /? G Su necht'L(/3) je jazyk všech w-slov, která mají stejnou příponu jako ß. Pak dvě slova u,v jsou ~l(/3) ekvivaletní, protože příslušnost w-slov ua, va do jazyka L(ß) vůbec naw, v nezávisí, a tedy ~l(/3) má pouze jednu třídu rozkladu. Zvolíme-li /? takové, že nemá nekonečný periodický rozvoj, pak zřejmě L(ß) není regulární (viz věta 1.14). Dále lze ukázat, že v tomto případě i kongruence ~ L^ má jen jednu třídu rozkladu.                                                                                                 D
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 největší kongruencí saturující L. Tento výsledek nás opravňuje nazvat S */~x syntaktickým monoidem, kde součinem je zřetězení tříd uvedeného rozkladu.
1.6   Modifikace Büchiho akceptační podmínky
V některých aplikacích, které j sou 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ý Büchiho automat je w-automat *4 = (A, Q)XS, kde A = (S, —>, Sin) je LTS nad S a Q = {G±,..., Gk \ Gi C S}. Vstupní w-slovo a je akceptováno, právě když existuje běh p na a takový, že platí: Vi.l < i < k : inf (p) n G i ^ 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ýchi nedeterministických) Büchiho automatů se třída akceptovaných jazyků nezmění. Při značení jako výše totiž platí:
k
L(A,g)  =  Q L(A,Gi).
í=i
Büchiho automat A' simulující automat A = {A,Q) lze zkonstruovat takto: při značení jako výše položíme A' = (S", S, —>', Sm', F), kde
S' = S x {1, ...,k}, Sin' = Sin x {1}, F = Gi x {1} a -V je definována takto:
(s,j) -^  (t,j)   je-li    s At, s £ G3
(sij) -^ (t, i) je-li s -^t, s e G j a kde i = (j mod k) + 1 . Ve druhé komponentě stavuje uchováván index j e [í, 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ěkterý stav z každé množiny G i 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í G i, G2,..., Gk, a tedy projít některým stavem z F nekonečně často.
Kapitola 2
Silnější akceptacní podmínky
Jak bylo ukázáno v předchozí kapitole, deterministické Bůchiho 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. Rovněž záměna akceptujích a neakceptuj ich stavů při komplementaci by nevedla k cíli - viz též poznámka 1.10. Zavedeme tedy silnější akceptacní podmínky, které, jak uvidíme, umožní definovat deterministické automaty rozponávající celou třídu w-regulárních jazyků.
2.1   Mullerovy automaty
Jednou z možností, jak obejít výše naznačené problémy, je specifikovat akceptacní podmínku tak, aby „akceptacní cyklus" v automatu obsahoval pouze samé akceptující stavy; takto zřejmě takto musíme specifikovat všechny akceptacní cykly. Následující definici zavedl Müller
MuUerův automat. Nechť A = (5, A, Sin) je konečně stavový LTS nad S. Řekneme, že
^-automat (A, Acc) je MuUerův automat, právě když Acc je tzv. Mullerova akceptacní
podmínka (MAC):
je dána množina fC2s podmnožin množiny stavů S (značená T = {Fľ, F2,..., Fk } a zvaná též Mullerova akceptacní tabulka). Slovo a : N0 —> £ je akceptováno, právě když existuje běh p : N0 —> S na slově a takový, že inf(p) G J-', tj. inf (p) = Fi pro nějaké i G {1,2,..., k}.
Tuto podmínku můžeme formálně zapsat takto:
(MAC)                           3p.(p(0) G Sin A Vi.(p(i) ^ P(i + 1)€A) A inf(p) G J7)
Uvedený MuUerův automat A značíme (A, T) nebo též (S, S, A, Sm,F). Jazyk rozpoznávaný (též akceptovaný) Mullerovým automatem A = (A, T) je množina
L(A) = {a G S" I A akceptuje a}
všech w-slov akceptovaných tímto automatem a značíme j ej též L(A, ľ).
17
18
KAPITOLA 2.  SILNEJŠÍAKCEPTACNIPODMÍNKY
Mullerova akceptační podmínka vskutku klade prísnej ši 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ě mnohoktrá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 (l\ Vi3j. j > i : p(j) = q A     f\   -Ni^j.j > i : p(j) = q) feT 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, 6}" všech slov takových, která obsahovala nekonečně mnoho výskytů symbolu a. A\ = ({si, s2j-, {a, b}, Ai, {si}, {si}) je deterministický automat s totální přechodovou funkcí a s Büchiho akceptační podmínkou {s i}.
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 = {{s i}, {si, s2}}. Dále jsme ukázali, že doplněkjazyka L není aceptovánžádnýmdeterministickýmBůchiho automatem. Snadno se ověří, že doplněkjazyka 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.                                                                                                    D
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.
Nechť (A, G), kde A = (5, —>, 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,JJa)'- libovolný úspěšný běh Büchiho automatu bude vyhovovat jedné z položek v Mullerově akceptační tabulce Tg ■ Obráceně, jakýkoli běh vyhovující některé položce z Tq musí projít některým stavem z G nekonečně mnohokrát.                                         D
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 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ý Mullerovův automat lze simulovat nedeterministickým Büchiho automatem. Nechť (A, T) je Mullerův automat, kde T = {Fi,F2,..., Fk}. Nejprve pro každé i, i = 1,..., k, zkonstruujeme Büchiho automat Ai = (Ai, G i) takový, že Ai akceptuje vstup a, právě když existuje běh p automatu (A, T) na a s vlastností inf(p) = Fi.
2.1. MULLEROVYAUTOMATY
19
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 — Fi, 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, -►, Sm) a f1» = {sh, sÍ2,..., sim }. Konstruujeme A = (Ai, G»), kde A = (5i;—>j, S\n) a Gj jsou definovány takto:
. S,i = S,u{(s,cyklusi,j) \seFi,je{0,l,...,m-í}}, 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 sij+1 počítán modulo m):
•
a
s —>i s                                                                  je-li    s —> s
s A, (s', cyklus^ 0)                                        je-li    s A s', s' <e F*
(s,cyklusť,j) -% (s,cyklusť,j)                      je-li    s A s\ s' e Fi, s =é 8ij+1
(s, cyklus^ j) -\ (s, cyklus^ (j + í) modm)    je-li    s A s', s' <e Fu s = sij+1
•   ^in = bin
• G» = {(sim,cyklusi; m-1)}
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ýchjazyků vůči sjednocení. Snadno se nahlédne, že L(A, F) = ULi L(^ Gi)-                                                                   D
Z právě uvedených lemmat plyne, že třída w-jazyků rozpoznatelných Mullerovými automaty j e totožná s třídou Buchi-rozpoznatelných (tj. w-regulárních) j azyků. Příklad 2.1 klade přirozenou otázku, zda deterministické Mullerovy automaty rozpoznávají celou třídu ^-regulárních jazyků; velmi netriviální důkaz, že tomu tak je podal McNaghton. Větu, která nese jeho jméno, uvádíme bez důkazu.
Veta 2.4. Každý uj-regulárníjazyk je rozpoznatelný něj akým deterministickým Mullerovým automatem.
Povšimněme si, že McNaghtonovavě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 J = 2s - F. Získáme tedy Mullerův automat (A, F), kde F = {F C S \ F £ F}. Snadno se nahlédne, že L (A, F) = Ľu - 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.
20
KAPITOLA 2.  SILNEJŠÍAKCEPTACNIPODMÍNKY
2.2   Rabínovy a Streetovy automaty
Důkaz McNaghtonovy 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. Nechť A = (S, A, Sm) je konečně stavový LTS nad S. Řekneme,
že w-automat (A, Acc) je Rabínův automat, právě když Acc je tzv. Rabínova akceptační
podmínka (RAC):
je dána množina VT C 2sx2s dvojic podmnožin množiny stavů S (značená VT = {(Gi, i?i), (G2, R'2), • • •, (Gfc, Rk)} a zvaná též Rabínova tabulka). Slovo a : N0 —> £ je akceptováno, právě když existuje běh p : N0 —> S na slově a takový, že 3i.l < i < k : inf (p) C\Gi^$ A inf (p) n Ri = 0.
Tuto podmínku můžeme formálně zapsat takto:
(RAC)                3p.(p(0) e Sin A Ví.(p® °^ P(i + 1) e A)
A 3i. 1 < i < k : inf (p) nG^ĚA  inf (p) n i?» = 0)
Uvedený Rabínův automat A značíme (A,VT) nebo též (5, S, A, Sin,VT). Jazyk rozpoznávaný (též akceptovaný) Rabinovým automatem A = (A, VT) je množina
L(A) = {a e Sw | A akceptuje a}
všech w-slov akceptovaných tímto automatem a značíme jej též L(A,VT).
Každá dvojice (Gi; Ri) 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 G i 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žujeme-li v Mullerově akceptační tabulce položku rV (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) O Gr =é 0 A inf (p) O Rr = 0 z RAC lze zapsat jako formuli 1. řádu takto:
V  (V v* ^ > *: ^') = i a A "^ ^ > *: ^^')= ^
r£{l,...,fc}  g£Gr                                                 geňr
Příklad 2.5. Vrátíme-li se opět k příkladu 1.4, pak L(A\) (nekonečně mnoho výskytů 'a') je akceptován Rabinovým automatem, který má LTS jako A i, s tabulkou obsahující jedinou dvojici ({si}, 0). Doplněk L(Ai) je akceptován Rabinovým automatem, který má opět tentýž LTS ajeho tabulka obsahuje jedinou dvojici ({s2J, {«i})-
2.2. RABÍNOVY'A STREETOVYAUTOMATY
21
Simulace
Büchiho automaty lze triviálně simulovat pomocí Rabínových automatů: je-li (A, F) Büchiho automat, pak ekvivaletní Rabínův automat je (A, VT F), kde VTF) = {{F, 0}}. (tj. 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í, zkonstraovatpro každou položku (R i; Gi) g VT jeden („izolovaný") Büchiho automat (Aí,Fí). Každý (Aí,Fí) 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 G i se objevuje v běhu nekonečně mnohokrát. Nastíněnou konstrukci nyní popišme formálně.
Nechť A = (S, -^, Sm) a VT = {(G1? Rx), (G2, R2),..., (Gk, Rk)}. Konstruujeme Ai = (Ai, Fi), kde Ai = (Si, —>i; S\n) a Gi jsou definovány takto:
. Si = S U {(s, cyklus,, j) I s g S - Ri, j g {0,1} } , • relace přechodu —>j je definována takto:
s —>i s                                                       je-li    S —> S
s -\ (s', cyklus,, 0)                       je-li   sAs
(s, cyklus,, 0) A, (s', cyklus,, 0)    je-li   s A s
(s, cyklus,, 0) A, (s', cyklus,, 1)    je-li   s A s
(s, cyklus,, 1) A, (s', cyklus,, 0)    je-li   s A s
s' £Ri
s' <£ Ri, s <£ Gi s' ^ Ri, s e Gi s' £Ri
• Fi = {(s,cyklus,, 1) \seS-Ri}
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 tabulku Ti =
{F C S I F n Gi # 0, F n Ri = 0} a hledaná Mullerova tabulka je T = Uie{1^k}Ti, což lze zapsat stručněji jako
k
T={FCS\  \/(F D Gi jí 9 A FnRi = 9)} . 1=1
Jelikožjsme LTS nijak nemodifikovali, platí, že simulující automatje deterministický, právě když simulovaný automatje 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), že deterministické Rabínovy automaty rozpoznávají celou třídu ^-regulárníchjazyků.
22
KAPITOLA 2.  SILNEJŠÍAKCEPTACNIPODMÍNKY
2.2.2 Streetův automat
Níže uvedenou akceptační podmínku, definovanou opět pomocí tabulky dvojic, zavedl poprvé Street (1988). Při nekonečných výpočtech j sou 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".
Streetův automat. Streetův automat je w-automat definovaný jako dvojice (A, VT), kde A = (S, A, Sm) aVT = {(Gu Rx), (G2, RA, ■ ■■, (Gk, Rk)} jsou definovány tak, jakou Rabínova automatu. Streetova akceptační podmínka (SAC) je definována takto:
Slovo a : N0 —> X je akceptováno, právě když existuje běh p : N0 —> S na slově a takový, že Vi.l < i < k : inf (p) n G» ^ 0 => inf (p) C\Ri^$. Tuto podmínku můžeme formálně zapsat takto:
(SAC)            3P-(p(Q) € Sm A Ví.(p(«) a^ p(i + 1) G A)
A Vi. 1 < i < k : inf (p) n Gi # 0 =>  inf (p) n i?i 7^ 0)
Uvedený Streetův automat *4 (opět) značíme (A, PT) nebo též (S,E,A,Sm,?T). Je tedy vždy nutno uvést, zda se jedná o interpretaci VT jako tabulky Rabínovy, či Streetovy, 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 R r 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 v*3-?--? > *:pti) = 1v V v*3-?--? > *:pti) = 1) ■
r£{l,...,k}        q£Gr                                                        q£Rr
Přímo z definice Streetova automatu se vidí jeho vztah k automatu Rabínovu:
Tvrzení 2.6. Nechť A = (A, VT) je automat s tabulkou dvojic. Nechť L r = L(A, VT), kde VT je interpretována jako Kabinová akceptační podmínka, a L s = L(A,VT), kde VT je interpretována jako Streetova akceptační podmínka. Pak L s je doplňkem Lr.
Simulace
Každý Büchiho automat (S, S, —>, Sin, F) je opět specálním případem Streetova automatu -stačí položit A; = l,G1= S,RX = f1 bez změny LTS (tj. PTF = {(S, G)} pro Streetovu interpretaci). O konstrukci Büchiho automatu simulujícího libovolný daný Streetův automat pojednává následující lemma (M. Vardi).
Lemma 2.7. Nechť A = (A, VT) je Streetův automat nad S, kde A = (S, —>, Sin), VT = {(Gi, i?i), (G2, R2), ■ ■ ■, (Gk, Rk)} an = card(S). Pak lze zkonstruovat Büchiho automat A' = (S', S, -►', S'm, F) takový, že L (A) = L (A)' a card(S') = n • 2°(fc).
2.2. RABÍNOVY'A STREETOVYAUTOMATY
23
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 (Gí,Rí) e VT. Automat A' tedy musí za uvedenou pozicí kontrolovatpro každé i implikaci: jestliže se některý ze stavů z G i vyskytuje nekonečně častokrát, pak i některý ze stavů z i? j 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 G i 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' = (S1, S, —>', S'in, F) zapsat takto:
. Si = SU{(s,X,Y) \seS, X,YC{l,2,...,k}},
•  relace přechodu —>' je definována takto:
s —>  s                                                    je-li    S —> S  .
s A' (s', 0,0)                                je-li    s A s', s' iRi,
(s, X, Y) A' (V, X U G, Y U R)   je-li    s A s', X U G % Y U R, kde
G = {i | s' e Gi,í < i < k} a R = {i | s' e Ri, 1 < i < k} ,
(s, X,Y) A' (s',XuG,0)           je-li    sAs',IuGCľufi;
•  F = {{s,X,W)\s&S,XQ{l,2,...,k}} .
D