Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic

Joseph Halpern, Leandro Rego

There has been a great deal of work on characterizing the complexity of the satisfiability and validity problem for modal logics. In particular, Ladner showed that the satisfiability problem for all logics between K and S4 is PSPACE-hard, while for S5, it is NP-complete. We show that it is negative introspection axiom that causes the gap: if we add this axiom to any modal logic between K and S4, then the satisfiability problem becomes NP-complete. Indeed, the satisfiability problem is NP-complete for any modal logic that includes the negative introspection axiom.

Subjects: 9.2 Computational Complexity


Submitted: Oct 15, 2006

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.