Automat Co-Büchi

W teorii automatów automat co-Büchi jest wariantem automatu Büchi . Jedyną różnicą jest warunek akceptacji: automat Co-Büchi akceptuje nieskończone słowo, $fa$ istnieje przebieg, tak że wszystkie stany występujące nieskończenie często w przebiegu są w stanie końcowym ustawionym $\ displaystyle w} F}$ . W przeciwieństwie do tego automat Büchi akceptuje słowo, $fa$ istnieje przebieg, tak że co najmniej jeden stan występujący nieskończenie często w stanie końcowym jest ustawiony $\ displaystyle F}$ .

(Deterministyczne) automaty Co-Büchi są ściśle słabsze niż (niedeterministyczne) automaty Büchi.

Definicja formalna

Formalnie deterministyczny automat ko-Büchi jest krotką ${\ Displaystyle {\ mathcal {A}} = (Q, \ Sigma, \ delta, q_ {0}, F )}$ , który składa się z następujących komponentów:

• ${\ displaystyle Q}$ to zbiór skończony . Elementy są $nazywane$ . _ $_$ _
• $\ Displaystyle \ Sigma}$${$ to skończony zwany alfabetem .
• $delta: Q \ razy \ Sigma \ rightarrow Q}$${\ Displaystyle {\ mathcal {A}}}$ jest funkcją przejścia ZA .
• ${0}}$$displaystyle$ jest elementem , zwanym stanem początkowym.
• ${\ displaystyle F \ subseteq Q}$ jest ostatecznym zestawem stanów . ${A}}}$${\ Displaystyle \ rho (w)}$ akceptuje dokładnie te słowa $biegiem ,$ w którym wszystkie nieskończenie często występujące stany w ${\ Displaystyle \ rho (w)}$ są w ${\ displaystyle F}$ .

W niedeterministycznym automacie ko-Büchi ${\ displaystyle \ Delta$ przejścia jest zastępowana relacją przejścia $}$ . Stan początkowy ${\ displaystyle Q_ {0}$ zastępowany zestawem stanów początkowych $}$ . Ogólnie termin automat co-Büchi odnosi się do niedeterministycznego automatu co-Büchi.

Aby zapoznać się z bardziej wszechstronnym formalizmem, zobacz także ω-automat .

Warunek akceptacji

Warunkiem akceptacji automatu co-Büchi jest formalnie

${\ Displaystyle \ istnieje i \ forall j: \; j \ geq i \ quad \ rho (w_ {j}) \ w F.}$

Warunek akceptacji Büchiego jest uzupełnieniem warunku akceptacji co-Büchiego:

${\ Displaystyle \ forall i \ istnieje j: \; j \ geq i \ quad \ rho (w_ {j}) \ w F.}$

Nieruchomości

Automaty Co-Büchi są zamknięte na sumę, przecięcie, projekcję i determinację.