In computer science and automata theory, a deterministic Büchi automaton is a theoretical machine which either accepts or rejects infinite inputs. Such a machine has a set of states and a transition function, which determines which state the machine should move to from its current state when it reads the next input character. Some states are accepting states and one state is the start state. The machine accepts an input if and only if it will pass through an accepting state infinitely many times as it reads the input. A non-deterministic Büchi automaton, later referred to just as a Büchi automaton, has a transition function which may have multiple outputs, leading to many possible paths for the same input; it accepts an infinite input if and only if some possible path is accepting. Deterministic and non-deterministic Büchi automata generalize deterministic finite automata and nondeterministic finite automaton to infinite inputs. Each are types of ω-automata. Büchi automata recognize the ω-regular languages, the infinite word version of regular languages. They are named after the Swiss mathematician Julius Richard Büchi, who invented them in 1962. Büchi automata are often used in model checking as an automata-theoretic version of a formula in linear temporal logic.
Formal definition
Formally, a deterministic Büchi automaton is a tuple A = that consists of the following components:
δ: Q × Σ → Q is a function, called the transition function of A.
q0 is an element ofQ, called the initial state of A.
F⊆Q is the acceptance condition. A accepts exactly those runs in which at least one of the infinitely often occurring states is in F.
In a 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.
Closure properties
The set of Büchi automata is closed under the following operations. Let A= and B= be Büchi automata and C= be a finite automaton.
Union: There is a Büchi automaton that recognizes the language L∪L.
Intersection: There is a Büchi automaton that recognizes the language L∩L.
Concatenation: There is a Büchi automaton that recognizes the language L⋅L.
ω-closure: If L does not contain the empty word then there is a Büchi automaton that recognizes the language Lω.
Complementation:There is a Büchi automaton that recognizes the language Σω/L.
Recognizable languages
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. ; Deterministic versus non-deterministic Büchi automata 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ω, 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ω 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ω. Contradiction. The class of languages recognizable by deterministic Büchi automata is characterized by the following lemma.
Algorithms
of finite state systems can often be translated into various operations on Büchi automata. In addition to the closure operations presented above, the following are some useful operations for the applications of Büchi automata. ; Determinization Since deterministic Büchi automata are strictly less expressive than non-deterministic automata, there can not be an algorithm for determinization of Büchi automata. But, McNaughton's Theorem and Safra's construction provide algorithms that can translate a Büchi automaton into a deterministic Muller automaton or deterministic Rabin automaton. ; Emptiness checking The language recognized by a Büchi automaton is non-empty if and only if there is a final state that is both reachable from the initial state, and lies on a cycle. An effective algorithm that can check emptiness of a Büchi automaton:
