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?