Büchi automaton
A
Büchi automaton is the extension of a
finite state automaton to infinite inputs. It accepts an infinite input sequence,
iff there exists a run of the automaton (in case of a deterministic automaton, there is exactly one possible run) which has infinitely many states in the set of final states.