Rabin's proofs of emptiness and complementation problems for automata on infinite trees 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."
 A: A modern perspective on Rabin's decidability theorem for S2S uses parity automata over infinite binary trees. These are nondeterministic top-down automata with a "parity ranking function" $\{\text{states}\} \to \mathbb{N}$; this function is involved in defining acceptance. (What you refer to as "exact acceptance condition on Büchi automata on trees" in the comments is in fact called the Muller condition in the literature; Rabin's original paper used yet another acceptance condition.)
For an introduction to parity automata, you may look for instance at Bojańczyk and Czerwiński's "Automata Toolbox" lecture notes. Its section 5.3 proves complementation (Lemma 5.6) and deduces from it the equivalence between definability in Monadic Second-Order logic and parity automata (Theorem 5.5). As for emptiness, it is reducible to solving parity games, which are treated in Chapters 2 and 3 of the Automata Toolbox.
Addendum: if you consider logical criteria of "simplicity", as in "what are the minimal axioms required to prove Rabin's theorem", that question has been studied in the framework of reverse mathematics by Kołodziejczyk and Michalewski.
