Crisp-Determinization of Weighted Tree Automata over Additively Locally Finite and Past-Finite Monotonic Strong Bimonoids Is Decidable

A weighted tree automaton is crisp-deterministic if it is deterministic and each of its transitions carries either the additive or multiplicative unit of the underlying weight algebra; weights different from these units may only appear at the root of the given input tree. A weighted tree automaton is crisp-determinizable if there exists an equivalent crisp-deterministic one. We prove that it is decidable whether weighted tree automata over additively locally finite and past-finite monotonic strong bimonoids are crisp-determinizable.