PSPACE bounds for rank-1 modal logics

DOI10.1145/1462179.1462185zbMATH Open1351.03015arXiv0706.4044OpenAlexW2250074872MaRDI QIDQ2946571FDOQ2946571

Authors: Lutz Schröder, Dirk Pattinson 

Publication date: 17 September 2015

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Abstract: For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics. Our main result is that all rank-1 logics enjoy a shallow model property and thus are, under mild assumptions on the format of their axiomatisation, in PSPACE. This leads to a unified derivation of tight PSPACE-bounds for a number of logics including K, KD, coalition logic, graded modal logic, majority logic, and probabilistic modal logic. Our generic algorithm moreover finds tableau proofs that witness pleasant proof-theoretic properties including a weak subformula property. This generality is made possible by a coalgebraic semantics, which conveniently abstracts from the details of a given model class and thus allows covering a broad range of logics in a uniform way.

Full work available at URL: https://arxiv.org/abs/0706.4044

Recommendations

• PSpace reasoning for graded modal logics
• scientific article; zbMATH DE number 1341607
• scientific article; zbMATH DE number 5046366
• PSPACE-decidability of Japaridze's polymodal logic
• Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic
• scientific article; zbMATH DE number 2196594
• scientific article; zbMATH DE number 1989649
• Lower bounds for modal logics
• A modal view on resource-bounded propositional logics
• Presburger Modal Logic Is PSPACE-Complete

zbMATH Keywords

resolutioncoalgebrashallow models

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Modal logic (including the logic of norms) (03B45) Categorical logic, topoi (03G30)

Cited In (21)

• Hybrid logic with the difference modality for generalisations of graphs
• Completeness for \(\mu\)-calculi: a coalgebraic approach
• Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics
• Coalgebraic Hybrid Logic
• Coalgebraic satisfiability checking for arithmetic \(\mu\)-calculi
• Coalgebraic semantics of modal logics: an overview
• Reasoning with Global Assumptions in Arithmetic Modal Logics
• Coalgebraic logics \& duality
• Title not available (Why is that?)
• COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description)
• Cut elimination in coalgebraic logics
• Free Heyting Algebras: Revisited
• On Composing Finite Forests with Modal Logics
• EXPTIME Tableaux for the Coalgebraic μ-Calculus
• The Temporal Logic of Coalitional Goal Assignments in Concurrent Multiplayer Games
• Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra
• A categorical approach to coalgebraic fixpoint logic
• Coalgebraic CTL: fixpoint characterization and polynomial-time model checking
• Cut Elimination for Shallow Modal Logics
• Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics
• Global caching for coalgebraic description logics

This page was built for publication: PSPACE bounds for rank-1 modal logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946571)