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.
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download
Contributor : Pierre Genevès <>
Submitted on : Wednesday, February 4, 2009 - 2:41:48 PM
Last modification on : Friday, October 25, 2019 - 2:01:11 AM
Long-term archiving on: Tuesday, June 8, 2010 - 8:08:43 PM


Files produced by the author(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. ⟨inria-00358797⟩



Record views


Files downloads