Complexity of Modal Logics with Presburger Constraints

Stéphane Demri (1, 2, 3) , Denis Lugiez (4)

1 LSV - Laboratoire Spécification et Vérification
2 CNRS - Centre National de la Recherche Scientifique
3 DAHU - Verification in databases
4 LIF - Laboratoire d'informatique Fondamentale de Marseille - UMR 6166

We introduce the extended modal logic EML with regularity constraints and full Presburger constraints on the number of children that generalize graded modalities, also known as number restrictions in description logics. We show that EML satisfiability is only pspace-complete by designing a Ladner-like algorithm. This extends a well-known and non-trivial pspace upper bound for graded modal logic. Furthermore, we provide a detailed comparison with logics that contain Presburger constraints and that are dedicated to query XML documents. As an application, we provide a logarithmic space reduction from a variant of Sheaves logic SL into EML that allows us to establish that its satisfiability problem is also pspace-complete, significantly improving the best known upper bound.

Mots clés: complexity; regularity constraint; arithmetical constraint; Ladner-like algorithm; modal logic; Presburger arithmetic; small model property

Domaines: Logique en informatique [cs.LO]

Stéphane Demri, Denis Lugiez. Complexity of Modal Logics with Presburger Constraints. Journal of Applied Logic, 2010, 8 (3), pp.233-252. ⟨10.1016/j.jal.2010.03.001⟩. ⟨hal-03188381⟩