Skip to Main content Skip to Navigation
New interface
Journal articles

Decidable Classes of Tree Automata Mixing Local and Global Constraints Modulo Flat Theories

Luis Barguñó 1 Carlos Creus 1 Guillem Godoy 1 Florent Jacquemard 2, 3 Camille Vacher 4, 5 
2 MuTant - Synchronous Realtime Processing and Programming of Music Signals
IRCAM - Institut de Recherche et Coordination Acoustique/Musique, Inria Paris-Rocquencourt, UPMC - Université Pierre et Marie Curie - Paris 6, CNRS - Centre National de la Recherche Scientifique
4 MOSTRARE - Modeling Tree Structures, Machine Learning, and Information Extraction
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
Abstract : We define a class of ranked tree automata TABG generalizing both the tree automata with local brother tests of Bogaert and Tison (1992) and with global equality and disequality constraints (TAGED) of Filiot et al. (2007). TABG can test for equality and disequality modulo a given flat equational theory between brother subterms and between subterms whose positions are defined by the states reached during a computation. In particular, TABG 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 TABG. 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 equivalence classes of subterms (modulo a given flat equational theory) reaching some state during a computation. We also adapt the model to unranked ordered terms. As a consequence of our results for TABG, we prove the decidability of a fragment of the monadic second order logic on trees extended with predicates for equality and disequality between subtrees, and cardinality.
Document type :
Journal articles
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Florent Jacquemard Connect in order to contact the contributor
Submitted on : Tuesday, August 20, 2013 - 6:33:07 PM
Last modification on : Tuesday, March 15, 2022 - 3:20:08 AM
Long-term archiving on: : Thursday, November 21, 2013 - 4:15:48 AM


Files produced by the author(s)


  • HAL Id : hal-00852382, version 1


Luis Barguñó, Carlos Creus, Guillem Godoy, Florent Jacquemard, Camille Vacher. Decidable Classes of Tree Automata Mixing Local and Global Constraints Modulo Flat Theories. Logical Methods in Computer Science, 2013, 9 (2), pp.1-39. ⟨hal-00852382⟩



Record views


Files downloads