Büchi automata are finite-state automata used to specify languages of infinite strings.
After J.R. Büchi, with an umlaut.
Büchi-automata are given as ordinary finite state automata, but their semantics is to specify infinitary languages, i.e., languages with infinite strings. Such an infinite string is accepted by the automaton iff its run (infinite computation) enters at least one of the final states infinitely often.
Nondeterministic Büchi-automata accept the so-called regular ω-languages. Their deterministic restriction is strictly weaker. In particular, there is no deterministic Büchi automaton that recognizes the language (0+1)*0ω, of infinite words in which 1 occurs only finitely often.
