I have originally asked this question on Math.SE, but I think it is more suitable here.

I have been reading M. Rabin's 1969 article Decidability of Second-Order Theories and Automata on Infinite Trees that proves the fact that *S2S* is decidable.

**Edit.** Let me elaborate a bit on the theory behind this, as suggested by Joel David Hamkins in the comments; *S2S* here denotes the monadic second-order theory of two successors, which is modelled by the full binary tree $T_2=\{0,1\}^*$. The automata Rabin uses in his article are so called **infinite tree automata** with Büchi acceptance conditions, which are (non-deterministic) automata that accept / reject $\Sigma$-valued infinite binary trees for an alphabet $\Sigma$ (eg. as is described on Wikipedia).

The proof that *S2S* is decidable relies on proofs of

Complementation problem(Theorem 1.5)Given an infinite tree automaton $\mathfrak A$, if $T(\mathfrak A)$ is f.a. definable, then so is its complement.

and

Emptiness problem(Theorem 1.6)For a given infinite tree automaton $\mathfrak A$, it is decidable if $T(\mathfrak A)=\emptyset$.

Contrary to automata on words and automata on finite trees, these two problems are not trivially decidable on *infinite* tree automata. Now Rabin proves the above two theorems in his paper, but as I have read in various more recent articles, the proofs Rabin gives are way too difficult. I have however not been able to find articles that actually give simpler proofs of the above theorems (apart from Rabin's 1972 *Automata on infinite objects and Church's Problem*, but the proof of the emptiness problem is still very tedious).

Now my question is, what is regarded as a good proof of the above two problems, or at least, is there an article that the authors of newer articles have in mind when saying things like "Rabin's proof is rather elaborate, but simpler proofs have subsequently been found."

2more comments