Complementation of $\omega$-regular languages in reverse mathematics 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$.
 A: There is a new paper addressing exactly this question:
L. A. Kołodziejczyk, H. Michalewski, P. Pradic, M. Skrzypczak, The logical strength of Büchi's decidability theorem
accepted to CSL 2016. The paper is available at the first author's website:
http://www.mimuw.edu.pl/~lak/buchi_strength.pdf.
The abstract states:

We prove that the following are equivalent over the weak second-order 
  arithmetic theory $\text{RCA}_0$:
  
  
*
  
*Büchi’s complementation theorem for nondeterministic automata on infinite words, 
  
*the decidability of the depth-n fragment of the MSO theory of (N, ≤), for each n ≥ 5, 
  
*the induction scheme for $\Sigma^0_2$ formulae of arithmetic.
  

A: This paper might be relevant: http://arxiv.org/abs/1508.06780.
It studies the complementation result for automata over infinite trees, rather than words.
There is a remark in this paper (page 11) concerning determinization of Buchi automata over ω-words:

We have not attempted a careful verification, but we believe that
  the proof of determinization 
  for word automata goes through in the fragment of
  ACA0 known as WKL0 extended by the induction scheme for Σ02
  formulas. Without Σ02
  induction, the basic notions of automata theory on infinite structures
  make little sense, in particular the lim inf of ranks appearing in a 
  computation might not exist.

Perhaps this remark can also be of help when considering complementation.
A: I am not familiar with all proofs of McNaughton's theorem, but the ones I have seen use the weak form of Konig's Lemma that a finitely branching infinite tree contains an infinite path.
