Multitree automata that count

Multitree are unranked, unordered trees and occur in many Computer Science applications like rewriting and logic, knowledge representation, XML queries, typing for concurrent systems, cryptographic protocols, etc. We define constrained multitree automata which accept sets of multitrees where the constraints are expressed in a first-order theory of multisets with counting formulas which is very expressive. We give constructions for union, intersection, determinization. Then, we give an algorithm to decide emptiness when the constraints belong to a subclass where counting is limited to distinct elements. We show that many classes of tree automata that have been defined for a wide variety of applications can be seen as instance of our general framework. Finally, we describe the quantifier elimination procedure used to decide the theory of constraints.