# 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.