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 visits (at least) one of the final states infinitely often. It is named after the Swiss mathematician Julius Richard Büchi who invented this kind of automaton in 1962.
Automata on infinite words are useful for...
more
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 visits (at least) one of the final states infinitely often. It is named after the Swiss mathematician Julius Richard Büchi who invented this kind of automaton in 1962.
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...
less
