Uzupełnienie automatu Büchi
W teorii automatów dopełnieniem automatu Büchiego jest konstrukcja innego automatu Büchiego , który rozpoznaje dopełnienie języka ω - regularnego rozpoznawanego przez dany automat Büchiego. Istnienie algorytmów dla tej konstrukcji dowodzi, że zbiór języków ω-regularnych jest domknięty pod względem dopełnienia.
Ta konstrukcja jest szczególnie trudna w porównaniu z konstrukcjami dla innych właściwości zamykania automatów Büchi . Pierwszą konstrukcję przedstawił Büchi w 1962 roku. Później opracowano inne konstrukcje, które umożliwiły sprawne i optymalne uzupełnienie.
Konstrukcja Büchiego
0 Büchi przedstawił podwójnie wykładniczą konstrukcję dopełnienia w logicznej formie. Tutaj mamy jego konstrukcję we współczesnej notacji stosowanej w teorii automatów. Niech A = ( Q ,Σ,Δ, Q , F ) będzie automatem Büchiego . Niech ~ A będzie relacją równoważności po elementach Σ + taką, że dla każdego v,w ∈ Σ + , v ~ A w wtedy i tylko wtedy, gdy dla wszystkich p,q ∈ Q , A ma bieg od p do q przez v jeśli i tylko wtedy, gdy jest to możliwe nad w , a ponadto A ma przebieg przez F od p do q przez v wtedy i tylko wtedy, gdy jest to możliwe nad w . Każda klasa ~ A definiuje odwzorowanie f : Q → 2 Q × 2 Q w następujący sposób: dla każdego stanu p ∈ Q mamy ( Q 1 , Q 2 )= f ( p ), gdzie Q 1 = { q ∈ Q | w może przenieść automat A z p do q } i Q 2 = { q ∈ Q | w może przenieść automat A z p do q poprzez stan w F }. Zauważ, że Q 2 ⊆ Q 1 . Jeśli f jest mapą definiowalną w ten sposób, oznaczamy (unikatową) klasę definiującą f przez L f .
Następujące trzy twierdzenia zapewniają konstrukcję dopełnienia A przy użyciu klas równoważności ~ A .
Twierdzenie 1: ~ A ma skończenie wiele równoważnych klas i każda klasa jest językiem regularnym . Dowód: Ponieważ istnieje skończenie wiele f : Q → 2 Q × 2 Q , relacja ~ A ma skończenie wiele klas równoważności. Pokażemy teraz, że L f jest językiem regularnym. Dla p , q ∈ Q i i ∈ {0,1} niech A ja , p , q = ( {0,1}× Q , Σ, Δ 1 ∪Δ 2 , {(0, p )}, {( i , q )} ) będzie niedeterministycznym automatem skończonym , gdzie Δ 1 = { ((0, q 1 ),(0, q 2 )) | ( q 1 , q 2 ) ∈ Δ} ∪ { ((1, q 1 ),(1, q 2 )) | ( q 1 , q 2 ) ∈ Δ} i Δ 2 = { ((0, q 1 ),(1, q 2 )) | q 1 ∈ fa ∧ ( q 1 , q 2 ) ∈ Δ }. Niech Q' ⊆ Q . Niech α p , Q' = ∩ { L ( ZA 1, p , q ) | q ∈ Q'}, który jest zbiorem słów, które mogą przenieść A z p do wszystkich stanów w Q' przez jakiś stan w F . Niech β p ,Q' = ∩{ L ( ZA 0, p , q )- L ( ZA 1, p , q )-{ε} | q ∈ Q'}, który jest zbiorem niepustych słów, które mogą przenieść A z p do wszystkich stanów w Q' i nie ma biegu przechodzącego przez żaden stan w F . Niech γ p ,Q' = ∩{ Σ + - L ( ZA 0, p , q ) | q ∈ Q'}, który jest zbiorem niepustych słów, które nie mogą przenieść A z p do żadnego ze stanów w Q'. Ponieważ języki regularne są zamknięte na skończonych przecięciach i na względnych dopełnieniach, każdy α p ,Q' , β p ,Q' i γ p ,Q' jest regularny. Z definicji L fa = ∩{ α p , Q 2 ∩ β p , Q 1 - Q 2 ∩ γ p , Q - Q 1 | ( Q 1 , Q 2 )= fa ( p ) ∧ p ∈ Q }.
000 Twierdzenie 2: Dla każdego w ∈ Σ ω istnieją ~ A klasy L f i L g takie, że w ∈ L f ( L g ) ω . Dowód: Użyjemy nieskończonego twierdzenia Ramseya, aby udowodnić to twierdzenie. Niech w = za za 1 ... i w ( ja , j ) = za ja ... za j -1 . Rozważ zbiór liczb naturalnych N . Niech klasy równoważności ~ A będą kolorami podzbiorów N o rozmiarze 2. Przypisujemy kolory w następujący sposób. Dla każdego i < j niech kolor { i , j } będzie klasą równoważności, w której występuje w ( i , j ). Z nieskończonego twierdzenia Ramseya możemy znaleźć nieskończony zbiór X ⊆ N taki, że każdy podzbiór X o rozmiarze 2 ma ten sam kolor. Niech 0 < ja < ja 1 < ja 2 .... ∈ X . Niech f będzie mapą definiującą klasę równoważności taką, że w (0, i ) ∈ L f . Niech g będzie mapą definiującą klasę równoważności taką, że dla każdego j > 0, w ( i j -1 , i j ) ∈ L g . Wtedy w ∈ L fa ( L sol ) ω .
00000000 Twierdzenie 3: Niech L f i L g będą klasami równoważności ~ A . Wtedy L f ( L g ) ω jest albo podzbiorem L ( A ) albo rozłącznym z L ( A ). Dowód: Załóżmy, że istnieje słowo w ∈ L ( A ) ∩ L f ( L g ) ω , w przeciwnym razie twierdzenie jest trywialne. Niech r będzie akceptującym przebiegiem A nad wejściem w . Musimy pokazać, że każde słowo w' ∈ L f ( L g ) ω jest również w L ( A ), tj. istnieje przebieg r' A nad wejściem w' taki, że stan w F występuje w r' w nieskończoność często. Ponieważ w ∈ L fa ( L g ) ω , niech w w 1 w 2 ... = w takie, że w ∈ L fa i dla każdego i > 0, w ja ∈ L g . Niech s i będzie stanem w r po spożyciu w ... w i . Niech I będzie zbiorem indeksów takich, że i ∈ I wtedy i tylko wtedy, gdy odcinek biegu w r od s i do s i +1 zawiera stan z F . Muszę być zbiorem nieskończonym. Podobnie możemy podzielić słowo w'. Niech w' w' 1 w' 2 ... = w' takie, że w' ∈ L f i dla każdego i > 0, w' i ∈ L g . Konstruujemy r' indukcyjnie w następujący sposób. Niech pierwszy stan r' będzie taki sam jak r . Zgodnie z definicją L f , możemy wybrać bieg segmentu na słowie w' , aby osiągnąć s . Zgodnie z hipotezą indukcyjną mamy przebieg w' ...w' i sięgający s i . Z definicji L g możemy rozszerzyć przebieg wzdłuż segmentu słowa w' i +1 tak, że rozszerzenie osiągnie s i+1 i odwiedzi stan w F jeśli i ∈ I . R' otrzymane z tego procesu będzie miało nieskończenie wiele segmentów przebiegów zawierających stany z F , ponieważ I jest nieskończone. Dlatego r' jest przebiegiem akceptującym, a w' ∈ L ( A ).
Za pomocą powyższych twierdzeń możemy przedstawić Σ ω - L ( A ) jako skończoną sumę języków ω-regularnych postaci L f ( L g ) ω , gdzie L f i L g są klasami równoważności ~ A . Dlatego Σ ω - L ( A ) jest językiem ω-regularnym. Możemy przetłumaczyć język na automat Büchi. Ta konstrukcja jest podwójnie wykładnicza pod względem wielkości A .