@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.}
}