# 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."

• Isn't the emptiness problem trivially decidable? Given an automaton, you just have to determine if you can reach an accepting state from the initial state. If so, there will be a word that is accepted. If not, then the language will be empty. Reachability in a finite digraph is decidable, since you just close the initial state under adjacency. Perhaps I've misunderstood your question? – Joel David Hamkins Jan 19 '17 at 14:23
• As is remarked in Rabin's article, or maybe some other article on this subject, this is not the case for (monadic) second-order logic on infinite trees. So, this question is not about finite words and standard DFA's, but rather about automata that can accept/reject valued infinite trees (eg. $T_2 = \{0,1\}^*$ with a map $v:T_2\to\Sigma$ that assigns a letter in some alphabet $\Sigma$ to every node) – konewka Jan 19 '17 at 14:26
• @JoelDavidHamkins To clarify a bit more, acceptance conditions on these so called Büchi automata are phrased in terms of states that are visited infinitely often on an (infinite) path $\pi$ in $T_2$, considered for all paths, hence the decision method you mentioned can not be reduced to the finite case. – konewka Jan 19 '17 at 14:33
• I would suggest, then, that you edit your question with fuller explanation about exactly what you are asking. For example, you don't mention Büchi automata in the question, but only finite-state automata. – Joel David Hamkins Jan 19 '17 at 14:35
• My general recommendation is that MO questions should provide a full context, since the audience here is extremely diverse. For example, I am expert in Büchi automata (whose emptiness problem is indeed trivially decidable by the argument I gave), but I haven't done much with Büchi automata on trees in the style of your question, which I understand only now after this back-and-forth. – Joel David Hamkins Jan 19 '17 at 14:49