
Suppose deterministic Buchi automaton \(A = (Q, \delta, q_0, F)\), we construct a (nondeterministic) Buchi automaton \(B = (Q', \Delta, q_0', F')\) such that \(L (B) = \Sigma^{\omega} \backslash L (A)\) as follows:
\(Q' = Q \times L\), where L={choice, end}
\(q_0' = (q_0, \operatorname{choice})\)
\(F' = \{ (s, \operatorname{end}) \mid s \in Q \}\)
\(\Delta\) is defined by following rules:
\((s', \operatorname{choice}) \in \Delta ((s, \operatorname{choice}), a)\) iff \(\delta (s, a) = s'\)
\((s', \operatorname{end}) \in \Delta ((s, \operatorname{choice}), a)\) iff \(\delta (s, a) = s' \wedge s' \not\in F\)
\((s', \operatorname{end}) \in \Delta ((s, \operatorname{end}), a)\) iff \(\delta (s, a) = s' \wedge s' \not\in F\)
Proof.
Suppose \(\rho\) is an accepting run of A, then \(\inf (\rho) \cap F \neq \emptyset\), there is at least a state q of F visited infinitely. If B goes into end states, it cannot enter any F states, thus \(\rho\) will not enter end states. So \(\rho\) is not accepted by B.
Suppose \(\rho\) is an accepting run of B, then \(\rho\) stays in end states from some point. Let that point be i. This means \(\rho\) will not enter any F states in A after reading the ith letter. Thus \(\rho\) is not accepted by A.