Size bound on Büchi automaton for complement

Question

For a given Büchi automaton $\mathcal A = (A, Q, \delta, q_0, F)$ we define a congruence on $A^{\ast}$ by $$ \begin{array}{llll} u \sim_{\mathcal A} v & :\Leftrightarrow & \mbox{for all }s,s' \in Q \mbox{ we have a path} \\ & & \mbox{from $s$ to $s'$ labeled by $v$ iff we have} \\ & & \mbox{such a path labeled by $w$ and} \\ & & \mbox{we have such a path which passes through a state from $F$} \\ & & \mbox{labeled by $v$ iff we have such a path labeled by $w$}. \end{array} $$ for $u, v \in A^{\ast}$. Now setting $W_{ss'} := \{ w \in A^{\ast} \mid \mbox{there is a path labeled $w$ from $s$ to $s'$}\}$ and $W_{ss'}^{F} := \{ w \in A^{\ast} \mid \mbox{there is a path labeled $w$ from $s$ to $s'$ going through a state in $F$}\}$ we have $$ [w]_{\sim_{\mathcal A}} = \bigcap_{\substack{s,s'\in Q \\ w \in W_{ss'}}} W_{ss'} \cap \bigcap_{\substack{s,s' \in Q \\ w \in A^{\ast} \setminus W_{ss'}}} A^{\ast}\setminus W_{ss'} \bigcap_{\substack{s,s'\in Q \\ w \in W_{ss'}^F}} W_{ss'}^F \cap \bigcap_{\substack{s,s' \in Q \\ w \in A^{\ast} \setminus W_{ss'}^F}} A^{\ast}\setminus W_{ss'}^F. $$ This equivalence is defined here and also in the the chapter Automata on infinite objects by Wolfgang Thomas in the Handbook of Theoretical Computer Science, Volume II. In this book it is said

Let us consider the complexity of the complementation process and the equivalence test. Given a Büchi automaton with $n$ states, there are $n^2$ different pairs $(s,s')$ and hence $O(2^{2n^2})$ different $\sim_{\mathcal A}$-classes. This leads to size bound of $O(2^{4n^2})$ states for the complement automaton.

As in the above formula, for each set $W_{ss'}$ (and $W_{ss'}^F$) we can decide wether it occurs in the intersection (and hence determines if one complement $A^{\ast}\setminus W_{ss'}$ and $A^{\ast} \setminus W_{ss'}^F$ occurs) we have $2^{n^2}\cdot 2^{n^2}$ options (different then $|Q^{2^{2Q}}|$ which would be given by the identification of the classes with functions $f : Q \to 2^Q \times 2^Q$ in the wikipedia article).

But why does this lead to a size bound of $O(2^{4n^2})$ for the complement automaton?

I do not see how to get a complement automaton such that this size bound could be easily seen?

Answer 1

Once you have the bound $2^{2n^2}$ on the number of classes, you can note that each state in the complement automaton corresponds to an $\omega$-regular language of the form $L_{f}L_{g}^\omega$, with $L_f$ and $L_g$ being functions from $Q$ to $2^Q\times 2^Q$.

Each such language is determined by $L_f$ and $L_g$, and there are $2^{2n^2}$ options for these functions, so you get a total of $(2^{2n^2})^2=2^{4n^2}$ options.

UPDATE FOLLOWING COMMENT: The correspondence of the number $2^{4n^2}$ to the states of the constructed automaton is not exact. Observe that for every language $L_f$, we can construct a nondeterministic NFA $A_f$ (as is done in Theorem 1 in the Wikipedia link you posted). Moreover, the size of $A_f$ is polynomial in the size of the original NBW $A$. Thus, the size of an NBW for $L_fL_g^\omega$ is polynomial. You then take a union of $2^{4n^2}$ such automata, and obtain the complement NBW, so the size of the complement NBW is: $$2^{4n^2}\cdot poly(n)=2^{4n^2 +\log poly(n)}=2^{O(4n^2)}$$ So it's a little less tight than $O(2^{4n^2})$, but it's still only singly exponential (perhaps there is a tighter analysis, but I'm not aware of one).