A Kleene theorem for weighted tree automata over tree valuation monoids (Q2280327)

The contribution establishes a Kleene theorem for weighted tree automata over tree valuation monoids as the title correctly announces. Weighted tree automata are essentially tree automata, in which each transition additionally carries a weight. Those weights are taken from a specific algebraic structure, which are tree valuation monoids in this contribution. Roughly speaking, a tree valuation monoid is a commutative monoid together with a valuation function that evaluates a tree of weights to a single weight. A Kleene theorem is a result that states that rational expressions (essentially corresponding to closure properties) and an automaton model coincide in expressive power. This result is achieved in the usual way. A weighted tree automaton is decomposed recursively into rational expressions and for the converse it is demonstrated that recognizable weighted tree languages, which are recognized by those weighted tree automata, have the required closure properties. As usual for tree automata additional concatenation leaf symbols (one for each state) are required for the transformation of a weighted tree automaton into an equivalent rational expression. The paper is well written and contains examples and illustrations for the benefit of the reader. All proof details are provided and no special background is required to appreciate the obtained results.