Complexity of modal logics with Presburger constraints (Q2638188)

This paper focuses on the study of a logical formalism introduced in order to query XML documents with arithmetical and regular constraints. Specifically, the authors introduce the Extended Modal Logic EML with regularity constraints and full Presburger constraints (more general than those in graded modal logics). The main result of the paper is that satisfiability in EML is PSPACE-complete, and its proof is by using a Ladner-like algorithm which generalizes existing results for graded modal logic. A comparison with logics that contain Presburger constraints and are used to query XML documents is given. As a consequence, PSPACE-completeness of a variant of Sheaves Logic is proved