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 i-th letter. Thus \(\rho\) is not accepted by A.