@inproceedings{Barcenas09a,
author = {Everardo Bárcenas and Pierre Genevès and Nabil Layaïda},
title = {Counting in Trees along Multidirectional Regular Paths},
booktitle = {PLAN-X'09, Proceedings of the ACM SIGPLAN Workshop
on Programming Language Techniques for XML},
location = {Savannah, GA, USA},
month = jan,
year = 2009,
url = {http://db.ucsd.edu/planx2009/papers.html},
url2 = {http://hal.inria.fr/inria-00358797/en/},
x-proceedings = {yes},
x-international-audience = {yes},
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.}
}