Counting Trees Along Multidirectional Regular Paths

Everardo Barcenas-Patino 1 Pierre Genevès 1 Nabil Layaïda 1
1 WAM - Web, adaptation and multimedia
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : We propose a tree logic capable of expressing simple cardinality constraints on the number of nodes selected by an arbitrarily deep regular path with backward navigation. Specifically, a sublogic of the alternation-free mu-calculus with converse for finite trees is extended with a counting operator in order to reason on the cardinality of node sets. Also, we developed a bottom-up tableau-based satisfiability-checking algorithm, which resulted to have the same complexity than the logic without the counting operator: a simple exponential in the size of a formula. This result can be seen as an extension of the so-called graded-modalities, which allows counting constraints only on immediate successors, with conditions on the number of nodes accessible by an arbitrary recursive and multidirectional path. This work generalizes the optimal complexity bound 2^O(n) where n is the length of the formula, shown by Geneves et al. in PLDI'07, for satisfiability of the logic extended with such counting constraints. Finally, we identify a decidable XPath fragment featuring cardinality constraints on paths with upward/downward recursive navigation, in the presence of XML types.
Type de document :
Communication dans un congrès
PLAN-X 2009, Jan 2009, Savannah, United States. 2009
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger
Contributeur : Pierre Genevès <>
Soumis le : mercredi 4 février 2009 - 14:41:48
Dernière modification le : jeudi 11 octobre 2018 - 08:48:03
Document(s) archivé(s) le : mardi 8 juin 2010 - 20:08:43


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00358797, version 1



Everardo Barcenas-Patino, Pierre Genevès, Nabil Layaïda. Counting Trees Along Multidirectional Regular Paths. PLAN-X 2009, Jan 2009, Savannah, United States. 2009. 〈inria-00358797〉



Consultations de la notice


Téléchargements de fichiers