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 automata 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 = (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.

Closure properties

The set of Büchi automata is closed under the following operations. Let and be Büchi automata and be a finite automaton.

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\cup 1)^* 0^\omega, 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\cup 1)^* 0^\omega with final state set F. A accepts 0^\omega. So, A will visit some state in F after reading some finite prefix of 0^\omega, say after the i_{0}th letter. A also accepts the ω-word Therefore, for some i_{1}, after the prefix the automaton will visit some state in F. Continuing with this construction the ω-word is generated which causes A to visit some state in F infinitely often and the word is not in (0\cup 1)^* 0^\omega. Contradiction. The class of languages recognizable by deterministic Büchi automata is characterized by the following lemma.

Algorithms

Model checking 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. 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. 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: Each of the steps of this algorithm can be done in time linear in the automaton size, hence the algorithm is clearly optimal. Minimizing deterministic Büchi automata (i.e., given a deterministic Büchi automaton, finding a deterministic Büchi automaton recognizing the same language with a minimal number of states) is an NP-complete problem. This is in contrast to DFA minimization, which can be done in polynomial time.

Variants

Transforming from other models of description to non-deterministic Büchi automata

From generalized Büchi automata (GBA)

From Linear temporal logic formula

From Muller automata

From Kripke structures

M = ⟨Q, I, R, L, AP⟩ where Q is the set of states, I is the set of initial states, R is a relation between two states also interpreted as an edge, L is the label for the state and AP are the set of atomic propositions that form L. (q, p) belongs to R and L(p) = a L(q) = a .

Complementation

In automata theory, complementation of a Büchi automaton is the task of complementing a Büchi automaton, i.e., constructing another automaton that recognizes the complement of the ω-regular language recognized by the given Büchi automaton. Existence of algorithms for this construction proves that the set of ω-regular languages is closed under complementation. This construction is particularly hard relative to the constructions for the other closure properties of Büchi automata. The first construction was presented by Büchi in 1962. Later, other constructions were developed that enabled efficient and optimal complementation.

Büchi's construction

Büchi presented a doubly exponential complement construction in a logical form. Here, we have his construction in the modern notation used in automata theory. Let A = (Q,Σ,Δ,Q0,F) be a Büchi automaton. Let ~A be an equivalence relation over elements of Σ+ such that for each v,w ∈ Σ+, v ~A w if and only if for all p,q ∈ Q, A has a run from p to q over v if and only if this is possible over w and furthermore A has a run via F from p to q over v if and only if this is possible over w. Each class of ~A defines a map f:Q → 2Q × 2Q in the following way: for each state p ∈ Q, we have (Q1,Q2)= f(p), where Q1 = {q ∈ Q | w can move automaton A from p to q} and Q2 = {q ∈ Q | w can move automaton A from p to q via a state in F}. Note that Q2 ⊆ Q1. If f is a map definable in this way, we denote the (unique) class defining f by Lf. The following three theorems provide a construction of the complement of A using the equivalence classes of ~A. Theorem 1: ~A has finitely many equivalent classes and each class is a regular language. Proof: Since there are finitely many f:Q → 2Q × 2Q, the relation ~A has finitely many equivalence classes. Now we show that Lf is a regular language. For p,q ∈ Q and i ∈ {0,1}, let Ai,p,q = ( {0,1}×Q, Σ, Δ1∪Δ2, {(0,p)}, {(i,q)} ) be a nondeterministic finite automaton, where Δ1 = { ((0,q1),(0,q2)) | (q1,q2) ∈ Δ} ∪ { ((1,q1),(1,q2)) | (q1,q2) ∈ Δ}, and Δ2 = { ((0,q1),(1,q2)) | q1 ∈ F ∧ (q1,q2) ∈ Δ }. Let Q' ⊆ Q. Let αp,Q' = ∩{ L(A1,p,q) | q ∈ Q'}, which is the set of words that can move A from p to all the states in Q' via some state in F. Let βp,Q' = ∩{ L(A0,p,q)-L(A1,p,q)-{ε} | q ∈ Q'}, which is the set of non-empty words that can move A from p to all the states in Q' and does not have a run that passes through any state in F. Let γp,Q' = ∩{ Σ+-L(A0,p,q) | q ∈ Q'}, which is the set of non-empty words that cannot move A from p to any of the states in Q'. Since the regular languages are closed under finite intersections and under relative complements, every αp,Q', βp,Q', and γp,Q' is regular. By definitions, Lf = ∩{ αp,Q 2 ∩ βp,Q 1-Q2 ∩ γp,Q-Q 1 Theorem 2: For each w ∈ Σω, there are ~A classes Lf and Lg such that w ∈ Lf(Lg)ω. Proof: We will use the infinite Ramsey theorem to prove this theorem. Let w =a0a1... and w(i,j) = ai...aj-1. Consider the set of natural numbers N. Let equivalence classes of ~A be the colors of subsets of N of size 2. We assign the colors as follows. For each i < j, let the color of {i,j} be the equivalence class in which w(i,j) occurs. By the infinite Ramsey theorem, we can find an infinite set X ⊆ N such that each subset of X of size 2 has same color. Let 0 < i0 < i1 < i2 .... ∈ X. Let f be a defining map of an equivalence class such that w(0,i0) ∈ Lf. Let g be a defining map of an equivalence class such that for each j>0,w(ij-1,ij) ∈ Lg. Then w ∈ Lf(Lg)ω. Theorem 3: Let Lf and Lg be equivalence classes of ~A. Then Lf(Lg)ω is either a subset of L(A) or disjoint from L(A). Proof: Suppose there is a word w ∈ L(A) ∩ Lf(Lg)ω, otherwise the theorem holds trivially. Let r be an accepting run of A over input w. We need to show that each word w' ∈ Lf(Lg)ω is also in L(A), i.e., there exists a run r' of A over input w' such that a state in F occurs in r' infinitely often. Since w ∈ Lf(Lg)ω, let w0w1w2... = w such that w0 ∈ Lf and for each i > 0, wi ∈ Lg. Let si be the state in r after consuming w0...wi. Let I be a set of indices such that i ∈ I if and only if the run segment in r from si to si+1 contains a state from F. I must be an infinite set. Similarly, we can split the word w'. Let w'0w'1w'2... = w' such that w'0 ∈ Lf and for each i > 0, w'i ∈ Lg. We construct r' inductively in the following way. Let the first state of r' be same as r. By definition of Lf, we can choose a run segment on word w'0 to reach s0. By induction hypothesis, we have a run on w'0...w'i that reaches to si. By definition of Lg, we can extend the run along the word segment w'i+1 such that the extension reaches si+1 and visits a state in F if i ∈ I. The r' obtained from this process will have infinitely many run segments containing states from F, since I is infinite. Therefore, r' is an accepting run and w' ∈ L(A). By the above theorems, we can represent Σω-L(A) as finite union of ω-regular languages of the form Lf(Lg)ω, where Lf and Lg are equivalence classes of ~A. Therefore, Σω-L(A) is an ω-regular language. We can translate the language into a Büchi automaton. This construction is doubly exponential in terms of size of A.