Equivalence, Unambiguity, and Sequentiality of Finitely Ambiguous Max-Plus Tree Automata

We show that the equivalence, unambiguity, and sequentiality problems are decidable for finitely ambiguous max-plus tree automata. A max-plus tree automaton is a weighted tree automaton over the max-plus semiring. A max-plus tree automaton is called finitely ambiguous if the number of accepting runs on every tree is bounded by a global constant and it is called unambiguous if there exists at most one accepting run on every tree. For the equivalence problem, we show that for two finitely ambiguous max-plus tree automata, it is decidable whether both assign the same weight to every tree. For the unambiguity and sequentiality problems, we show that for every finitely ambiguous max-plus tree automaton, both the existence of an equivalent unambiguous automaton and the existence of an equivalent deterministic automaton are decidable.