Complementation of Büchi automaton

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 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 → 2^Q × 2^Q in the following way: for each state p ∈ Q, we have (Q₁,Q₂)= f(p), where Q₁ = {q ∈ Q | w can move automaton A from p to q} and Q₂ = {q ∈ Q | w can move automaton A from p to q via a state in F}. Note that Q₂ ⊆ Q₁. If f is a map definable in this way, we denote the (unique) class defining f by L_f.

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 → 2^Q × 2^Q, the relation ~_A has finitely many equivalence 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 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, 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 the 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. 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 < 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. Then w ∈ L_f(L_g)^ω.

Theorem 3: Let L_f and L_g be equivalence classes of ~_A. Then L_f(L_g)^ω is either a subset of L(A) or disjoint from L(A).
Proof: Suppose there is a word w ∈ L(A) ∩ L_f(L_g)^ω, otherwise the theorem holds trivially. Let r be an 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 exists a run r' of A over input w' such that a state 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 if and only if 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 the 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. 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 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.