Complementation of Büchi automaton

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,Σ,Δ,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.