3
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks so far. For the Büchi case, I actually could have derived it myself differently, but I didn't think of that when I posted the question: Since I knew that one cannot determinize nondeterministic Büchi word automata (without switching to another type of acceptance condition), I could simply have seen that if it would work for trees, it would in particular work for the special case of unary trees, that is, words, which is a contradiction. Your counterexample is also convincing, and it helps to see it that way. $\endgroup$ – TrojanWhoresProcurer Mar 16 '20 at 14:29
  • $\begingroup$ Do you by any chance know it for the case of parity tree automata? For parity word automata it works, but I really couldn't find any results on trees here. $\endgroup$ – TrojanWhoresProcurer Mar 16 '20 at 14:29
  • 1
    $\begingroup$ @TrojanWhoresProcurer The proof idea should hold for all types of non-deterministic tree automata (well, except for safety), including parity tree automata. $\endgroup$ – DCTLib Mar 16 '20 at 14:41
  • $\begingroup$ Just to make sure I understand it correctly: By "the proof idea" you mean similar to your counterexample? In other words, for all types of nondeterministic tree automata (except safety), their deterministic versions are strictly less expressive? $\endgroup$ – TrojanWhoresProcurer Mar 16 '20 at 14:46
  • $\begingroup$ @TrojanWhoresProcurer Exactly. $\endgroup$ – DCTLib Mar 16 '20 at 15:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.