Composed Bisimulation for Tree Automata

We address the problem of reducing the size of (nondeterministic,bottom-up) tree automata using suitable, language-preservingequivalences on the states of the automata. In particular, we proposethe so-called composed bisimulation as a new language preservingequivalence. Composed bisimulation is defined in terms of two differentrelations, namely upward and downward bisimulation. Moreover, weprovide simple and efficient algorithms for computing composedbisimulation based on a reduction to the problem of computingbisimulations on (labeled) transition systems. The proposal of composedbisimulation is motivated by an attempt to obtain an equivalence thatcan provide better reductions than what currently knownbisimulation-based approaches can offer, but which is not significantlymore difficult to compute (and hence stays below the computationalrequirements of simulation-based reductions). The experimental resultswe present in the paper show that our composed bisimulation meets suchrequirements, and hence provides users of tree automata with a finerway to resolve the trade-off between the available degree of reductionand its cost.