The Emptiness Problem for Tree Automata with Global Constraints

We define tree automata with global constraints (TAGC), generalizing the well-known class of tree automata with global equality and disequality constraints [14] (TAGED). TAGC can test for equality and disequality between subterms whose positions are defined by the states reached during a computation. In particular, TAGC can check that all the subterms reaching a given state are distinct. This constraint is related to monadic key constraints for XML documents, meaning that every two distinct positions of a given type have different values. We prove decidability of the emptiness problem for TAGC. This solves, in particular, the open question of decidability of emptiness for TAGED. We further extend our result by allowing global arithmetic constraints for counting the number of occurrences of some state or the number of different subterms reaching some state during a computation. We also allow local equality and disequality tests between sibling positions and the extension to unranked ...

• Type: Journal
• Year: 2010
• Where: LICS
• Authors: Luis Barguñó, Carles Creus, Guillem Godoy, Florent Jacquemard, Camille Vacher
• Keywords: Automated Reasoning, Disequality, LICS 2010, Positions, TAGC