Bottom-Up Tree Automata with Term Constraints

We introduce bottom-up tree automata with equality and disequality term constraints. These constraints are more expressive than the equality and disequality constraints between brothers introduced by Bogaert and Tison in 1992. Our new class of automata is still closed under Boolean operations. Moreover, we show that for tree automata with term constraints not only membership but also emptiness is decidable. This contrasts with the undecidability of emptiness for automata with arbitrary equality constraints between subterms identified by paths as shown in 1981 by Mongy.