A Büchi automaton is like a finite state machine (FSM) except that it accepts infinite inputs. An FSM accepts an input if it enters an accepting state once; a Büchi automaton accepts an input if it passes through an accepting state infinitely many times.
As with FSMs, there are deterministic and non-determistic variants of Büchi automata but, unlike FSMs, not all non-deterministic automata can be converted to deterministic Büchi automata. (See [Wikipedia page] for details/alternatives.)
Büchi automata are used for model checking by converting linear temporal logic formulae to automata. They can accept any ω-regular language.
Notes related to Büchi automaton
Papers related to Büchi automaton
- Software model checking [jhala:compsurv:2009]