Global Numerical Constraints on Trees

TL;DR

This paper presents a new logical framework for reasoning about numerical constraints on tree structures, enabling concise expression of occurrence bounds across various regions, with applications to XML and XPath queries.

Contribution

The introduced logic can express numerical bounds on any tree region, is decidable in exponential time, and supports reasoning tasks like emptiness and containment for XML schemas and XPath queries.

Findings

Decidable in single exponential time with binary constraints

Expresses numerical bounds on any tree region including ancestors and descendants

Enables reasoning about XML schemas and XPath query extensions

Abstract

We introduce a logical foundation to reason on tree structures with constraints on the number of node occurrences. Related formalisms are limited to express occurrence constraints on particular tree regions, as for instance the children of a given node. By contrast, the logic introduced in the present work can concisely express numerical bounds on any region, descendants or ancestors for instance. We prove that the logic is decidable in single exponential time even if the numerical constraints are in binary form. We also illustrate the usage of the logic in the description of numerical constraints on multi-directional path queries on XML documents. Furthermore, numerical restrictions on regular languages (XML schemas) can also be concisely described by the logic. This implies a characterization of decidable counting extensions of XPath queries and XML schemas. Moreover, as the logic is closed under negation, it can thus be used as an optimal reasoning framework for testing emptiness, containment and equivalence.