Definition
Büchi Automaton
A Büchi automaton is an automaton similar to a deterministic finite automata.
In contrast to DFA, Büchi automata operate over an infinite set of words over , called the -words. The set of all infinite words is denoted as .