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.
Document type :
Conference papers
PLAN-X 2009, Jan 2009, Savannah, United States. 2009


https://hal.inria.fr/inria-00358797
Contributor : Pierre Genevès <>
Submitted on : Wednesday, February 4, 2009 - 2:41:48 PM
Last modification on : Tuesday, February 17, 2009 - 5:42:05 PM
Document(s) archivé(s) le : Tuesday, June 8, 2010 - 8:08:43 PM

File

counting.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00358797, version 1

Collections

Citation

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>

Share

Metrics

Record views

303

Document downloads

95