Pushing for Weighted Tree Automata

Explicit pushing for weighted tree automata over semifields is introduced. A careful selection of the pushing weights allows a normalization of bottom-up deterministic weighted tree automata. Automata in the obtained normal form can be minimized by a simple transformation into an unweighted automaton followed by unweighted minimization. This generalizes results of Mohri and Eisner for deterministic weighted string automata to the tree case. Moreover, the new strategy can also be used to test equivalence of two bottom-up deterministic weighted tree automata M-1 and M-2 in time O(vertical bar M vertical bar log vertical bar Q vertical bar), where vertical bar M vertical bar = vertical bar M-1 vertical bar + vertical bar M-2 vertical bar and vertical bar Q vertical bar is the sum of the number of states of M-1 and M-2. This improves the previously best running time O(vertical bar M-1 vertical bar . vertical bar M-2 vertical bar) .