Can one determinize finite automata over infinite trees?

Question

I'm currently considering deterministic, nondeterministic, universal, and alternating automata over infinite words and trees, with Büchi, co-Büchi, Muller, Rabin, Streett, or parity acceptance conditions.

I know that over words, all these automata accept the same languages, except deterministic and universal Büchi automata, as well as deterministic and nondeterministic co-Büchi automata.

I also know that over trees, nondeterministic and alternating Muller, Rabin, Streett, and parity automata accept the same languages, and strictly more languages than nondeterministic and alternating Büchi automata.

But I hardly know anything about deterministic tree automata, and I'm having a hard time finding more in the literature. And this captures my main question, whether one can determinize nondeterministic automata over infinite trees.

After all, they are definitely used. For example, in reactive LTL synthesis, we often convert the formula to a nondeterministic Büchi word automaton, then to a deterministic parity word automaton, from which we derive a deterministic parity tree automaton.

Also note that I didn't mention the co-Büchi case when it comes to trees. I just know that, again in reactive LTL synthesis, we can alternatively convert the negated formula to a nondeterministic Büchi word automaton, then to a universal co-Büchi word automaton for the original formula, from which we can derive a universal co-Büchi tree automaton. But that alone doesn't really say anything about the relation of deterministic parity tree automata and universal co-Büchi tree automata, or does it?

Answer 1

This may be not explicitly spelled at many places in the literature, as deterministic tree automata are unable to capture specifications that are only expressible in branching-time logics.

Take for instance the property "There exists a node in the tree labeled with atomic proposition $x$" - this is equivalent to the CTL formula $\mathit{EF\,} x$. This one cannot be represented as a deterministic tree automaton, but is easy to express as a non-deterministic Büchi tree automaton. The reason is that a tree automaton accepts a tree $\langle T, \tau \rangle$ if all branches in the run tree for $\langle T, \tau \rangle$ are accepting. With non-determinstic tree automata, one can route the obligation to see an $x$ to somewhere in the tree. With deterministic automata, this is just not possible and thus one can only express $\mathit{AF}\, x$ in this form.

Hence, non-deterministic tree automata cannot be determinized in general.