Büchi automaton

In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence if there exists a run of the automaton that visits (at least) one of the final states infinitely often. Büchi automata recognize the omega-regular languages, the infinite word version of regular languages. It is named after the Swiss mathematician Julius Richard Büchi who invented this kind of automaton in 1962. In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence if there exists a run of the automaton that visits (at least) one of the final states infinitely often. Büchi automata recognize the omega-regular languages, the infinite word version of regular languages. It is named after the Swiss mathematician Julius Richard Büchi who invented this kind of automaton in 1962. Büchi automata are often used in model checking as an automata-theoretic version of a formula in linear temporal logic. Formally, a deterministic Büchi automaton is a tuple A = (Q,Σ,δ,q0,F) that consists of the following components: In a non-deterministic Büchi automaton, the transition function δ is replaced with a transition relation Δ that returns a set of states, and the single initial state q0 is replaced by a set I of initial states. Generally, the term Büchi automaton without qualifier refers to non-deterministic Büchi automata. For more comprehensive formalism see also ω-automaton. The set of Büchi automata is closed under the following operations. Let A=(QA,Σ,ΔA,IA,FA) and B=(QB,Σ,ΔB,IB,FB) be Büchi automata and C=(QC,Σ,ΔC,IC,FC) be a finite automaton. Büchi automata recognize the ω-regular languages. Using the definition of ω-regular language and the above closure properties of Büchi automata, it can be easily shown that a Büchi automaton can be constructed such that it recognizes any given ω-regular language. For converse, see construction of a ω-regular language for a Büchi automaton. The class of deterministic Büchi automata does not suffice to encompass all omega-regular languages. In particular, there is no deterministic Büchi automaton that recognizes the language (0∪1)*0ω, which contains exactly words in which 1 occurs only finitely many times. We can demonstrate it by contradiction that no such deterministic Büchi automaton exists. Let us suppose A is a deterministic Büchi automaton that recognizes (0∪1)*0ω with final state set F. A accepts 0ω. So, A will visit some state in F after reading some finite prefix of 0ω, say after the i0th letter. A also accepts the ω-word 0i010ω. Therefore, for some i1, after the prefix 0i010i1 the automaton will visit some state in F. Continuing with this construction the ω-word 0i010i110i2... is generated which causes A to visit some state in F infinitely often and the word is not in (0∪1)*0ω. Contradiction.