DBA complement

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.