thumb|200px|Niedetermistyczny automat Büchiego który rozpoznaje (0∪1)*0ω
Automat Büchiego (ang. Büchi automaton) to rozszerzenie automatu skończonego na słowa nieskończone. Automat Büchiego składa się z: alfabetu, zbioru stanów z wyróżnionym stanem startowym oraz podzbiorem stanów akceptujących, funkcji przejścia, która pobiera aktualny stan oraz literę alfabetu i zwraca nowy stan (deterministyczne automaty Büchiego), lub relacji przejścia, która może zwracać wiele stanów (niedeterministyczne automaty Büchiego).
Słowo (nieskończone) jest akceptowane przez automat Büchiego, jeśli stan akceptujący wystąpi w tym słowie nieskończenie wiele razy.
W przeciwieństwie do zwykłych automatów skończonych, gdzie automaty deterministyczne i niedeterministyczne miały taką samą moc, niedeterministyczne automaty Büchiego są silniejsze od deterministycznych.
Niedeterministyczne automaty Büchiego są zamknięte ze względu na dopełnienie, przecięcie i alternatywę.
Dopełnienie automatu deterministycznego może być automatem niedeterministycznym.
Algorytm budowania dopełniania automatu Poniższy algorytm nie jest poprawny dla dowolnych niedeterministycznych automatów Buchiego. Poprawne konstrukcje, np.