|
|
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.
Automata on infinite words are useful for specifying behavior of nonterminating systems, such as hardware or operating systems. For such systems, you may want to specify a property such as "for every request, an acknowledge eventually follows", or its negation "there is a request which is not followed by an acknowledge". The latter is a property of infinite words: you cannot say of a finite sequence that it satisfies this property.
Büchi automata recognize the omega-regular languages, the infinite word version of regular languages. A language defined by a Rabin automaton, Streett automaton, parity automaton, or Muller automaton is also omega-regular. These automata have more powerful acceptance conditions, and are therefore often more succinct (use fewer states to express the same language).
A minor variant of Büchi automata is the generalized Büchi automaton, which has more than one set of accepting states. A run is accepting if it passes through every accepting state infinitely often. Multiple acceptance conditions can be gotten rid of with help of the "counting construction"
The class of deterministic Büchi automata does not accept all omega-regular languages. In particular, there is no deterministic Büchi automaton that accepts the language (a+b)*a^{omega}. (Any word that has an infinite suffix consisting of only a's.) This language is recognized by a two-state nondeterministic Büchi automaton.
Just like any automaton, Büchi automata can also be seen as tree automata.
Büchi automata are often used in Model checking as a automata-theoretic version of a formula in linear temporal logic.
See also
- Wolfgang Thomas, Automata on infinite objects, in Van Leeuwen, Ed., Handbook of Theoretical Computer Science, pp. 133-164, Elsevier, 1990.de:Büchi-Automat