Counting in trees for free

International audienceIn [22], it was shown that MSO logic for ordered unranked trees becomes undecidable if Presburger constraints are allowed at children of nodes. We now show that a decidable logic is obtained if we use a a modal fixpoint logic instead. We present an automata theoretic characterization of this logic by means of deterministic Pres-burger tree automata (PTA) and show how it can be used to express numerical document queries. Surprisingly, the complexity of satisfiability for the extended logic is asymptotically the same as for the original logic. The non-emptiness for PTAs is in general pspace-complete which is moderate given that it is already pspace-hard to test whether the complement of a regular expression is non-empty. We also identify a subclass of PTAs with a tractable non-emptiness problem. Further, to decide whether a tree t satisfies a formula $\phi$ is polynomial in the size of $\phi$ and linear in the size of t. A technical construction of independent interest is a linear time construction of a Presburger formula for the Parikh set of a finite automaton