7738996294

((2) => (3)) Weźmy dowolny NBA A o stanach Q. stanie początkowym qj i stanach akceptujących F. Z twierdzenia Kleenego, dla każdych p,q € Q istnieje wyrażenie regularne L_p>q opisujące te słowa skończone, w których automat A ma pewien bieg z p do q. Wówczas wyrażenie w-regulame opisujące słowa akceptowane przez A to:

U ww

g€F

((2) =» (1))

Odpowiednia formuła jest prawie taka sama jak na poprzednim wykładzie. Należy jedynie podmienić ostatni warunek na mówiący, że nieskończenie często występuje tranzycja, której stan docelowy jest akceptujący. Jest to formula postaci V_x3_y>_x y € X, gdzie X to zbiór pozycji korzystających z tranzycji o docelowym stanie akceptującym.

((!)=> (2))

Przeprowadzimy indukcję po strukturze danej formuły.

Należy pokazać, że języki rozpoznawane przez automaty NBA są zamknięte na wszystkie operacje z logiki MSO:

•    U wynika to z tego, że są to automaty niedeterministyczne.

•    3 (rzutowanie) obsługujemy za pomocą niedeterminizmu, w identyczny sposób jak na poprzednim wykładzie.

•    fi wyraża się przez U i Można też zrobić konstrukcję bezpośrednio na automatach, bez korzystania ze skomplikowanej operacji dla dopełnienia.

•    -i (dopełnienie) jest treścią reszty tego wykładu, znajduje się w rozdziale 2.3.

2.3 Dopełnienie dla NBA

W celu zakończenia dowodu twierdzenia Buchiego, wystarczy udowodnić następujący lemat:

Lemat 5. Niech L C AA będzie językiem rozpoznawanym przez NBA. Wówczas A* — L też jest rozpoznawany przez NBA.

Reszta tego rozdziału to dowód powyższego lematu. Niech A będzie NBA akceptującym L o zbiorze stanów Q i zbiorze stanów akceptujących F. Chcemy stworzyć automat B taki, że dla dowolnego w € A^w:

A nie akceptuje w <=> B akceptuje w

Równoważnie, B ma akceptować słowa, w których każdy bieg automatu A przechodzi skończenie wiele razy przez stany akceptujące z F.

Uwaga. Nie działa następująca naiwna konstrukcja automatu B:

Stanami automatu B są podzbiory zbioru Q. Stanem automatu B po przeczytaniu słowa aia2...a_n jest zbiór stanów, jakie A może mieć po przeczytaniu aia2-..a„ (w szczególności stanem początkowym automatu B jest zbiór stanów początkowych automatu >1).

Niech dane będzie słowo nieskończone w = ai<i2... i niech P_n C Q będzie stanem automatu B po przeczytaniu prefiksu aia2...a„. Warunkiem akceptacji przez automat B słowa w jest:

3,V_n>,P„ (1F = 0

(od pewnego momentu już nie ma stanów akceptujących automatu A). Warunek ten nie jest warunkiem typu Buchiego, ale łatwo automat zmienić na NBA: trzeba niedeterministycznie wybierać moment, od którego nie ma stanów akceptujących.

13