Counting in Trees for Free
Helmut Seidl, Thomas Schwentick, Anca Muscholl, Peter Habermehl · 2004
In [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 Presburger 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 # is polynomial in the size of # and linear in the size of t.