Andreas Reuß and Helmut Seidl. Bottom-up Tree Automata with Term Constraints. In Christian G. Fermüller and Andrei Voronkov, editors, LPAR-17, volume 6397 of LNCS, pages 581-593, 2010. Springer.

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.

Reference: Bibtex The original publication is available at