Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics

Yevgeny Kazakov, Ian Pratt-Hartmann

TL;DR

This work classifies the satisfiability problem for graded modal logic over all frame classes formed by intersections of reflexive, serial, symmetric, transitive, and Euclidean properties. It shows a trichotomy: $\mathsf{PSPACE}$-completeness when Euclidean and transitive features are absent, $\mathsf{NP}$-completeness when Euclidean or symmetry+transitivity conditions are present, and $\mathsf{NExpTime}$-completeness when transitivity is present without Euclidean or symmetry. Key techniques include a normal-form transformation and exponential-size model bounds to obtain $\mathsf{NExpTime}$ membership for transitive cases, and a polynomial-time reduction to $\mathcal{C}^1$ for Euclidean frames to obtain $\mathsf{NP}$-hardness and an NP upper bound. The results hold under both unary and binary coding of numerical subscripts, clarifying the complexity landscape of graded modal logics and informing related description-logics and semantic tableau methods.

Abstract

Graded modal logic is the formal language obtained from ordinary (propositional) modal logic by endowing its modal operators with cardinality constraints. Under the familiar possible-worlds semantics, these augmented modal operators receive interpretations such as "It is true at no fewer than 15 accessible worlds that...", or "It is true at no more than 2 accessible worlds that...". We investigate the complexity of satisfiability for this language over some familiar classes of frames. This problem is more challenging than its ordinary modal logic counterpart--especially in the case of transitive frames, where graded modal logic lacks the tree-model property. We obtain tight complexity bounds for the problem of determining the satisfiability of a given graded modal logic formula over the classes of frames characterized by any combination of reflexivity, seriality, symmetry, transitivity and the Euclidean property.

A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics

TL;DR

This work classifies the satisfiability problem for graded modal logic over all frame classes formed by intersections of reflexive, serial, symmetric, transitive, and Euclidean properties. It shows a trichotomy: -completeness when Euclidean and transitive features are absent, -completeness when Euclidean or symmetry+transitivity conditions are present, and -completeness when transitivity is present without Euclidean or symmetry. Key techniques include a normal-form transformation and exponential-size model bounds to obtain membership for transitive cases, and a polynomial-time reduction to for Euclidean frames to obtain -hardness and an NP upper bound. The results hold under both unary and binary coding of numerical subscripts, clarifying the complexity landscape of graded modal logics and informing related description-logics and semantic tableau methods.

Abstract

Graded modal logic is the formal language obtained from ordinary (propositional) modal logic by endowing its modal operators with cardinality constraints. Under the familiar possible-worlds semantics, these augmented modal operators receive interpretations such as "It is true at no fewer than 15 accessible worlds that...", or "It is true at no more than 2 accessible worlds that...". We investigate the complexity of satisfiability for this language over some familiar classes of frames. This problem is more challenging than its ordinary modal logic counterpart--especially in the case of transitive frames, where graded modal logic lacks the tree-model property. We obtain tight complexity bounds for the problem of determining the satisfiability of a given graded modal logic formula over the classes of frames characterized by any combination of reflexivity, seriality, symmetry, transitivity and the Euclidean property.

Paper Structure

This paper contains 7 sections, 24 theorems, 24 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Euclidean frames
  4. Transitive frames
  5. Membership in $\mathsf{NExpTime}$
  6. $\mathsf{NExpTime}$-hardness
  7. Conclusion

Key Result

Theorem 1

Let $\mathcal{F} \subseteq \{\hbox{\rm Rfl}, \hbox{\rm Ser}, \hbox{\rm Sym}, \hbox{\rm Tr} , \hbox{\rm Eucl} \}$, with $\hbox{\rm Eucl} \in \mathcal{F}$ or $\{\hbox{\rm Sym}, \hbox{\rm Tr}\} \subseteq \mathcal{F}$. Then the satisfiability problem for ordinary modal logic over $\bigcap \mathcal{F}$ i

Figures (2)

  • Figure 1: The set of z-worlds generated by Formulas \ref{['eq:generate0']}--\ref{['eq:character6']}.
  • Figure 2: Creating o-worlds (shown as a hollow dots) and the grid using Formulas \ref{['eq:standard1:h']}--\ref{['eq:standard3:v']} ($n=3$): g-worlds (shown as filled dots) are arranged according to their coordinates at the base; g-worlds which are horizontal neighbours in this grid have a common horizontal o-world successor, while g-worlds which are vertical neighbours in this grid have a common vertical o-world successor.

Theorems & Definitions (24)

  • Theorem 1
  • Theorem 2
  • Theorem 3
  • Theorem 4
  • Theorem 5
  • Theorem 6: logic:kuncak+rinard07logic:ph08
  • Lemma 1
  • Lemma 2
  • Lemma 3
  • Lemma 4
  • ...and 14 more