bchi automaton

A Bchi 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. Bchi 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 Bchi automata is the generalized buechi 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 Bchi automata does not accept all omega-regular languages. In particular, there is no deterministic Bchi automaton that accepts the language (a+b)*a^{omega}. (Any word that has an inifinite suffix consisting of only a's.) This language is recognized by a two-state nondeterministic Bchi automaton. Just like any automaton, Bchi automata can also be seen as tree automata. Bchi automata are often used in Model checking as a automata-theoretic version of a formula in linear temporal logic.

Bchi Automaton

See also