Automata for unordered trees

We present a framework for defining automata for unordered data trees that is parametrised by the way in which multisets of children nodes are described. Presburger tree automata and alternating Presburger tree automata are particular instances. We establish the usual equivalence in expressiveness of tree automata and MSO for our framework. We then investigate subclasses of automata for unordered trees for which testing language equivalence is in P-time. Starting from automata in our framework that describe multisets of children by finite automata, we propose two approaches to do this deterministically. We show that confluent horizontal evaluation leads to polynomial-time emptiness and universality, but coNP-complete emptiness and intersection. Finally, efficient algorithms can be obtained by imposing an order of horizontal evaluation globally for all automata in the class. Depending on the choice of the order, we obtain different classes of automata, each of which has the same expressiveness as Counting Mso.