Complexity of modal logics with Presburger constraints

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. Key words: modal logic, Ladner-like algorithm, arithmetical constraint, regularity constraint, computational complexity

• Type: Journal
• Year: 2010
• Where: JAPLL
• Authors: Stéphane Demri, Denis Lugiez
• Keywords: JAPLL 2010, Logic, Modal Logic, Regularity Constraint