# Complementation of Büchi automaton

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,Σ,Δ,Q$_0$,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$_1$,Q$_2$)= f(p), where Q$_1$ = {q ∈ Q | w can move automaton A from p to q} and Q$_2$ = {q ∈ Q | w can move automaton A from p to q via a state in F}. Note that Q$_2$ ⊆ Q$_1$. 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, Σ, Δ$_1$∪Δ$_2$, {(0,p)}, {(i,q)} ) be a nondeterministic finite automaton, where Δ$_1$ = { ((0,q$_1$),(0,q$_2$)) | (q$_1$,q$_2$) ∈ Δ} ∪ { ((1,q$_1$),(1,q$_2$)) | (q$_1$,q$_2$) ∈ Δ}, and Δ$_2$ = { ((0,q$_1$),(1,q$_2$)) | q$_1$ ∈ F ∧ (q$_1$,q$_2$) ∈ Δ }. 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$_1$,Q$_2$)=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$_0$a$_1$... 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$_0$ < i$_1$ < i$_2$ .... ∈ X. Let f be a defining map of an equivalence class such that w(0,i$_0$) ∈ 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$_0$w$_1$w$_2$... = w such that w$_0$ ∈ L$_f$ and for each i > 0, w$_i$ ∈ L$_g$. Let s$_i$ be the state in r after consuming w$_0$...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'$_0$w'$_1$w'$_2$... = w' such that w'$_0$ ∈ 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'$_0$ to reach s$_0$. By induction hypothesis, we have a run on w'$_0$...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.