Counting and Equality Constraints for Multitree Automata

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.... We define constrained multitree automata which accept sets of multitrees where the constraints are expressed in a first-order theory of multisets with counting formulae which is very expressive and decidable. The resulting class of multitree automata is closed under boolean combination, has a decidable emptiness problem and we show that this class strictly embeds all previous classes of similar devices which have been defined for a whole variety of applications.