Complementation of Büchi automaton

In automata theory, complementation of a Büchi automaton is construction of another Büchi automaton that recognizes 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 and Büchi automata are 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.^[1] Later, other constructions were developed that enabled efficient and optimal complementation.^[2][3][4][5]

Büchi's construction

Büchi presented^[1] 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,Σ,Δ,Q₀,F) be a Büchi automaton. Let ~_A be an equivalence relation over elements of Σ⁺ such that for each v,w ∈ Σ⁺, v ~_A w iff for all p,q ∈ Q, A has a run from p to q over v iff this is possible over w and furthermore A has a run via F from p to q over v iff this is possible over w. By definition, each map f:Q → 2^Q × 2^Q defines a class of ~_A. We denote the class by L_f. We interpret f in the following way. w ∈ L_f iff, for each state p ∈ Q and (Q₁,Q₂)= f(p), w can move automaton A from p to each state in Q₁ and to each state in Q₂ via a state in F. Note that Q₂ ⊆ Q₁. The following three theorems provides 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 → 2^Q × 2^Q, ~_A has finitely many equivalent classes. Now we show that L_f is a regular language. For p,q ∈ Q and i ∈ {0,1}, let A_i,p,q = ( {0,1}×Q, Σ, Δ₁∪Δ₂, {(0,p)}, {(i,q)} ) be a nondeterministic finite automaton, where Δ₁ = { ((0,q₁),(0,q₂)) | (q₁,q₂) ∈ Δ} ∪ { ((1,q₁),(1,q₂)) | (q₁,q₂) ∈ Δ}, and Δ₂ = { ((0,q₁),(1,q₂)) | q₁ ∈ F ∧ (q₁,q₂) ∈ Δ }. Let Q' ⊆ Q. Let α_p,Q' = ∩{ L(A_1,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(A_0,p,q)-L(A_1,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(A_0,p,q) |q ∈ Q'}, which is the set of non-empty words that can not move A from p to any of the states in Q'. By definitions, L_f = ∩{ α_p,Q2∩ β_p,Q1-Q2∩ γ_p,Q-Q1 |(Q₁,Q₂)=f(p) ∧ p ∈ Q}.

Theorem 2: For each w ∈ Σ^ω, there are ~_A classes L_f and L_g such that w ∈ L_f(L_g)^ω.
Proof: We will use infinite Ramsey theorem to prove this theorem. Let w =a₀a₁... and w(i,j) = a_i...a_j-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. Due to infinite Ramsey theorem, we can find infinite set X ⊆ N such that each subset of X of size 2 has same color. Let 0 < i₀ < i₁ < i₂ .... ∈ X. Let f be a defining map of an equivalence class such that w(0,i₀) ∈ L_f. Let g be a defining map of an equivalence class such that for each j>0,w(i_j-1,i_j) ∈ L_g. Therefore, w ∈ L_f(L_g)^ω.

Theorem 3: Let L_f and L_g be equivalence classes of ~_A. L_f(L_g)^ω is either subset of L(A) or disjoint from L(A).
Proof: Lets suppose word w ∈ L(A) ∩ L_f(L_g)^ω. Otherwise theorem holds trivially. Let r be the accepting run of A over input w. We need to show that each word w' ∈ L_f(L_g)^ω is also in L(A), i.e., there exist a run r' of A over input w' such that states in F occurs in r' infinitely often. Since w ∈ L_f(L_g)^ω, let w₀w₁w₂... = w such that w₀ ∈ L_f and for each i > 0, w_i ∈ L_g. Let s_i be the state in r after consuming w₀...w_i. Let I be a set of indices such that i ∈ I iff the run segment in r from s_i to s_i+1 contains a state from F. I must be an infinite set. Similarly, we can split the word w'. Let w'₀w'₁w'₂... = w' such that w'₀ ∈ L_f and for each i > 0, w'_i ∈ L_g. We construct r' inductively in the following way. Let first state of r' be same as r. By definition of L_f, we can choose a run segment on word w'₀ to reach s₀. By induction hypothesis, we have a run on w'₀...w'_i that reaches to s_i. By definition of L_g, we can extend the run along the word segment w'_i+1 such that the extension reaches s_i+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 set. Therefore, r' is an accepting run and w' ∈ L(A).

Due to the above theorems, we can represent Σ^ω-L(A) as finite union of ω-regular languages of the from L_f(L_g)^ω, where L_f and L_g 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.

References

1. Büchi, J. R. (1962), "On a decision method in restricted second order arithmetic", Proc. International Congress on Logic, Method, and Philosophy of Science, Stanford, 1960, Stanford: Stanford University Press, pp. 1–12.
2. McNaughton, R. (1966), "Testing and generating infinite sequences by a finite automaton", Information and Control 9: 521–530, doi:10.1016/s0019-9958(66)80013-x.
3. Sistla, A. P.; Vardi, M. Y.; Wolper, P. (1987), "The complementation problem for Büchi automata with applications to temporal logic", Theoretical Computer Science 49: 217–237, doi:10.1016/0304-3975(87)90008-9.
4. Safra, S. (October 1988), "On the complexity of ω-automata", Proc. 29th IEEE Symposium on Foundations of Computer Science, White Plains, New York, pp. 319–327.
5. Kupferman, O.; Vardi, M. Y. (July 2001), "Weak alternating automata are not that weak", ACM Transactions on Computational Logic 2 (2): 408–429.