From TheBestLinks.com
(Redirected from
Buechi automaton)
pl:Automat Büchi'ego
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 Buechi automata is the generalized buechi automaton, which has more then 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 Buechi automata does not accept all omega-regular languages. In particular, there is no deterministic Buechi 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 Buechi automaton.
Just like any automaton, Buechi automata can also be seen as tree automata.
Buechi 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.
Related links
Top visited
0 of
0 links
[no links posted yet]
>> place link >>
Discussion
Last posted
0 of
0 messages
[no messages posted yet]
>> post message >>
Watch
You can
add this article to your own "watchlist" and receive e-mail notification about all changes in this page.
