Seonglae ChoA finite-state machine that decides whether a desired state recurs forever in a never-ending system execution.
- A Büchi automaton extends DFAs/NFAs to infinite-length inputs (ω-words). A run is accepted if it visits an accepting state infinitely often.
- This makes it possible to express infinitely running systems, such as "does some condition keep holding / recur from now on?", and it is widely used in LTL-based model checking.
- Nondeterministic Büchi automata are strictly more expressive than deterministic ones. As a class they characterize exactly the ω-regular languages, but a general Büchi automaton cannot always be converted into a deterministic Büchi automaton.
