Helmut Seidl. Single-Valuedness of Tree Transducers is Decidable in Polynomial Time. Theor. Comput. Sci., 106(1):135-181, 1992.
A bottom-up finite-state tree transducer (FST) A is called single-valued iff for every input tree there is at most one output tree. We give a polynomial-time algorithm which decides whether or not a given FST is single-valued. The algorithm is based on: the freedom of the submonoid of trees which contain at least one occurrence of one variable *; the succinct representation of trees by graphs; a sequence of normalizing transformations of the given transducer; and a polynomially decidable characterization of pairs of equivalent output functions. We apply these methods to show that finite-valuedness is decidable in polynomial time as well.