Does anyone know where Büchi's theorem that $\omega$-regular languages are closed under complementation fits into the reverse-mathematics classification scheme? That is, is it equivalent over $\mathrm{RCA}_0$ to one of the usual subsystems of second-order arithmetic? Or, if not known to be equivalent, what is known about where it fits in?
The formulation I have in mind is, for a fixed finite signature $\Sigma$, the statement: for every finite automaton $M$ (over $\Sigma$), there exists a finite automaton $M^c$, such that, for every $\omega$-word $\alpha$ over $\Sigma$, it holds that $\alpha$ is (Büchi-)accepted by $M$ if and only if $\alpha$ is not accepted by $M^c$.
