  We present an efficient algorithm to reduce the size of nondeterministic tree
automata, while retaining their language. It is based on new transition pruning
techniques, and quotienting of the state space w.r.t. suitable equivalences. It
uses criteria based on combinations of downward and upward simulation preorder
on trees, and the more general downward and upward language inclusions. Since
tree-language inclusion is EXPTIME-complete, we describe methods to compute
good approximations in polynomial time. We implemented our algorithm as a
module of the well-known libvata tree automata library, and tested its
performance on a given collection of tree automata from various applications of
libvata in regular model checking and shape analysis, as well as on various
classes of randomly generated tree automata. Our algorithm yields substantially
smaller and sparser automata than all previously known reduction techniques,
and it is still fast enough to handle large instances.

Formal Languages and Automata Theory