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.
Büchi automaton
In computer science and automata theory, a deterministic Büchi automaton is a theoretical machine which either accepts or rejects infinite inputs. Such a machine has a set of states and a transition function, which determines which state the machine should move to from its current state when it reads the next input character. Some states are accepting states and one state is the start state. The machine accepts an input if and only if it will pass through an accepting state infinitely many times as it reads the input.
https://en.wikipedia.org/wiki/B%C3%BCchi_automaton
