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

Joseph Y. Halpern; Leandro Chaves Rego

REVIEW

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

Logic in Computer Science · Submitted 5 Mar 2006 · 2 references

Pith's verdict: The 'iff A5' complexity split looks correct, but Lemma 3.2's small-model proof has a real gap: the Euclidean 'standard arguments' miss formulas where KKψ is not a subformula, and a concrete example shows the construction can fail.

T0 · AI review

How this review was made: An AI referee (deepseek-v4-flash) read the paper on August 28, 2026 and answered a fixed list of questions about it. T0 is the starting level every paper gets. The levels describe how deeply Pith has checked the paper, never the authors.

T0 AI review An AI read the paper and answered a fixed list of questions.
T1 Audit Automatic checks that the references and files the paper relies on exist and match.
T2 Compute The paper's code or calculations re-run with the same results.
T3 Formal statement The claims written out in a formal math language a computer can read.
T4 Proof Those claims proved, and the proof checked by computer.

How Pith checks papers →

· 1 major objection · 5 minor · Ask about this paper · The compiled record · Read the full review →

Challenge this review Comment (0) Read on arXiv ↗

Cite ▾

arXiv IDcs/0603019 (version 1)

Pith IDGM3SEWT6, Pith's permanent record of this paper and its review

CitationJoseph Y. Halpern, Leandro Chaves Rego. "Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic." arXiv:cs/0603019 (2006). https://pith.science/paper/GM3SEWT6

Cite this reviewBibTeX for Pith's review of this paper

Claim paper

Why Pith says this

Highlight any text to comment on it.

Editor's note

read the letter

Here's my take on Halpern–Rego. The headline result — modal satisfiability is NP-complete exactly when negative introspection A5 is present, PSPACE-complete otherwise — is a clean, useful way to package known complexity results, and I believe it's correct. The paper does a good job of setting up the axiom/property correspondence and being upfront that the proof uses standard techniques. The unified statement is new as far as I know, and it's a genuinely helpful organizing fact for epistemic modeling.

The soft spot is real, though. Lemma 3.2's proof of the NP upper bound for pure Euclidean frames (C={e}) has a gap. In the key step, when a state s in S fails Kψ' while s0 satisfies Kψ', the proof says 'standard arguments' show s0 satisfies ¬KKψ', so Kψ' lands in F2. That's not valid for arbitrary Euclidean relations: you only get the witness for Kψ' in the small model if KKψ' is actually a subformula of φ, and that need not be the case. The stress-test example is right: φ = K(¬Kp ∧ p) ∧ ¬K¬p is satisfiable in a simple Euclidean model, but the construction as written leaves out the state that falsifies p, and the resulting small model fails φ. So the proof of the NP upper bound for C={e} isn't supported as written.

I don't think this sinks the theorem. K5 satisfiability is known to be NP-complete, and a modified argument — adding witnesses for all Kψ that fail inside the cluster, then re-checking the size bound — will likely repair the lemma. But the paper needs to do that work. The PSPACE-side 'straightforward modifications' and the claim that F2 is empty when e is combined with r or t are also sketched rather than proved, though those are minor by comparison.

Bottom line: this is a paper worth engaging with — the characterization is genuinely useful and the proof strategy is sound in outline — but it needs a revised Lemma 3.2 before the central claim is fully established. I'd send it to review; a knowledgeable referee can check the fix.

Referee report

Major objections (1)

[Section 3, Lemma 3.2] The converse direction of Lemma 3.2 is not proved as written. In the induction step for ψ = Kψ′, the proof argues that if (M′,s) |= ¬Kψ′ and (M′,s0) |= Kψ′, then “standard arguments using the fact that K′ is Euclidean” give (M′,s0) |= ¬KKψ′, and concludes “Thus Kψ′ ∈ F2.” This conclusion is valid only if KKψ′ is a subformula of φ, because F2 was defined as the set of subformulas Kψ such that KKψ is a subformula of φ and (M′,s0) |= ¬KKψ ∧ Kψ. That subformula condition is not guaranteed. Concretely, let φ = K(¬Kp ∧ p) ∧ ¬K¬p. This formula is satisfiable in the Euclidean model with states r, s, t, K(r)={s}, K(s)=K(t)={s,t}, p true at r and s and false at t. Running the construction of Lemma 3.2 gives F1={K¬p} and S={s}; F2=∅ because neither KK¬p nor KKp is a subformula of φ, so S′=∅. The constructed model has states {r,s} with K(r)=K(s)={s} and p true at both, and at r the conjunct K(¬Kp ∧ p) fails because s |= Kp. Thus the construction does not preserve φ. Since the NP upper bound for C={e} depends entirely on this lemma, this is a load-bearing gap. The lemma can likely be repaired, for example by redefining F2 as the set of all subformulas Kψ with (M′,s0) |= ¬KKψ ∧ Kψ, and by supplying an explicit construction for the witness state that does not require KKψ to be a subformula; the size bound would still hold because F1 and F2 are disjoint sets of distinct K-subformulas. As written, however, the proof is incorrect and the upper bound is unsupported.

Minor objections (5)

[Section 1, p.2] The sentence “the system A4 is T + A4” should read “the system S4 is T + A4”; as printed it is self-referential and confusing.
[Abstract and Section 1, p.1] “There has been a great of work” should be “There has been a great deal of work.”
[Section 3, proof of Theorem 3.1] The NP-hardness lower bound for C={e} is not explicitly stated. It can be obtained immediately from Ladner's NP-completeness result for S5, since every S5 model is an Me model; the authors should state this explicitly rather than only saying they “generalize” the NP-completeness argument.
[Section 3, proof of Theorem 3.1] The PSPACE-completeness for the cases e∉C beyond Ladner's original list (namely C={t}, C={s}, C={t,s}) is dismissed as “straightforward to modify.” A brief sentence indicating why Ladner's technique adapts to seriality and transitivity separately, or a precise reference, would make the proof self-contained.
[Section 3, Lemma 3.2] The remark immediately after the definition of F2, stating that F2=∅ when e and at least one of r or t is in C, is made before the construction is defined; moving it after the construction or adding a forward reference would improve readability.

How Pith checks papers → · Full audit of this paper →

The paper

The paper claims

Modal satisfiability is NP-complete exactly when the axiom of negative introspection, $\neg Kp \Rightarrow K\neg Kp$, is present; without it the problem is PSPACE-complete.

The reading

The paper's central claim is a dichotomy: in single-agent modal logic, the satisfiability problem is NP-complete exactly when the Euclidean condition is imposed on the accessibility relation, and PSPACE-complete otherwise. In axiomatic terms, the line is drawn by negative introspection, $\neg Kp \Rightarrow K\neg Kp$ (axiom A5). This matters because earlier work located the NP-PSPACE gap in a different axiom, the ability to combine knowledge; this paper shows that a single axiom about not knowing draws the same boundary. The proof extends a small-model characterization to the Euclidean-only case and derives all other Euclidean cases from it.

What carries the argument

The load-bearing object is the small-model characterization in Lemma 3.2. It says that a formula $\varphi$ is satisfiable in a Euclidean model iff it is satisfiable in a model with at most $|\varphi|$ states, built from a root $s_0$, a set $S$ containing one falsifying witness for every knowledge formula $K\psi$ that is false at the root, and a set $S'$ containing falsifying witnesses for formulas $K\psi$ that the root knows but does not know that it knows. The Euclidean condition forces the accessibility relation on this small model to be uniform, with every non-root state seeing exactly $S \cup S'$, and that uniformity is what makes polynomial-time model checking possible after an NP guess of the small structure.

Extended reading notes

Core claim

Theorem 3.1 states that for every subset $C$ of $\{r,e,t,s\}$, deciding whether a formula $\varphi \in LK_1(\Phi)$ is satisfiable in $M_C(\Phi)$ is NP-complete if $e \in C$, and PSPACE-complete if $e \notin C$. Via the standard correspondence between frame conditions and axioms, this means satisfiability is NP-complete precisely for those logics whose axioms include negative introspection (A5), and PSPACE-complete for those that do not. The new technical content is the case $C=\{e\}$: the authors prove that satisfiability in the class of Euclidean frames can be decided by guessing a model of at most $|\varphi|$ states of a special shape, and the other Euclidean cases reduce to this case or to earlier S5 and KD45 results.

Load-bearing premise

The proof's NP upper bound rests on the step in Lemma 3.2 where, if a reachable state fails $K\psi$ while the root satisfies $K\psi$, 'standard arguments' using Euclideanness are said to imply that the root fails $KK\psi$; the construction of the second-layer witness set $S'$ depends on that implication, which is not valid for arbitrary Euclidean relations.

Editorial extensions

If this is right

For every modal logic built on the base system K by adding any subset of the knowledge axiom (A3), positive introspection (A4), and negative introspection (A5), satisfiability is NP-complete if A5 is present and PSPACE-complete otherwise.
The complexity boundary is insensitive to reflexivity, transitivity, and seriality: once the Euclidean condition is fixed, adding or removing those conditions does not change the complexity class.
KD45-style logics of belief, which include A5, inherit NP-completeness, while logics of knowledge such as T, K4, and S4, which lack A5, remain PSPACE-complete.
Because validity is the complement of satisfiability for negated formulas, the same axiom boundary separates co-NP-completeness from PSPACE-completeness for validity in the same logics.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Beyond the paper: the axiom-level reading suggests a broader principle that the NP/PSPACE boundary in normal modal logics may be governed by the presence of a negative-introspection-like axiom; testing this on graded or probabilistic modal logics would be a direct next step.
Beyond the paper: the small-model shape in Lemma 3.2 gives a practical recipe, since a SAT solver can decide satisfiability in Euclidean modal logics by guessing one state per knowledge subformula, so the result transfers naturally to bounded model checking.
Beyond the paper: the false-step risk in Lemma 3.2 makes a precise question worth asking: does every $M^e$-satisfiable formula already have a small model of the lemma's shape, or only a small Euclidean model of some other shape? Answering that would either repair the proof or replace it.

Original abstract

There has been a great of work on characterizing the complexity of the satisfiability and validity problem for modal logics. In particular, Ladner showed that the validity problem for all logics between K, T, and S4 is {\sl PSPACE}-complete, while for S5 it is {\sl NP}-complete. We show that, in a precise sense, it is \emph{negative introspection}, the axiom $\neg K p \rimp K \neg K p$, that causes the gap. In a precise sense, if we require this axiom, then the satisfiability problem is {\sl NP}-complete; without it, it is {\sl PSPACE}-complete.

The compiled record

The paper's own sentences, arranged, kept beside the review and separate from it. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.

Compiled by classifier-1.13-20260917 via OpenRouter, question bank abstract-p1-20260923, 2026-09-23: 1 request, 3,686 input tokens, $0.0002 reported.

What the abstract itself states, as probabilities: claims first 0.05 · states limitation 0.11 · human participants 0.02 · controlled comparison 0.13 · randomized assignment 0.01 · states quantitative result 0.22 · compares with prior results 0.86 · mentions code or data availability 0.02.

The abstract, sentence by sentence

arXiv listing abstract v1. Results and the main claim are underlined; show every role.

There has been a great of work on characterizing the complexity of the satisfiability and validity problem for modal logics. In particular, Ladner showed that the validity problem for all logics between K, T, and S4 is {\sl PSPACE}-complete, while for S5 it is {\sl NP}-complete. We show that, in a precise sense, it is \emph{negative introspection}, the axiom $\neg K p \rimp K \neg K p$, that causes the gap. In a precise sense, if we require this axiom, then the satisfiability problem is {\sl NP}-complete; without it, it is {\sl PSPACE}-complete.

background contribution method result interpretation main claim

What the classifier reports for each sentence. The number is the probability it gave the label.
#	sentence	role	the authors' own work	states the main conclusion	strength
s0	There has been a great of work on characterizing the complexity of the satisfiability and validity problem for modal logics.	background 1.00	0.03	0.02	asserted 0.99
s1	In particular, Ladner showed that the validity problem for all logics between K, T, and S4 is {\sl PSPACE}-complete, while for S5 it is {\sl NP}-complete.	background 0.99	0.03	0.03	asserted 1.00
s2	We show that, in a precise sense, it is \emph{negative introspection}, the axiom $\neg K p \rimp K \neg K p$, that causes the gap.	result 0.61	0.91	0.76	asserted 1.00
s3	In a precise sense, if we require this axiom, then the satisfiability problem is {\sl NP}-complete; without it, it is {\sl PSPACE}-complete.	result 0.98	0.93	0.86	asserted 1.00

What kind of paper the classifier reports this is: theoretical result 1.00 · evidence from proof or derivation 0.97.

What was examined, and what was not

sources read

arXiv listing abstract v1

not examined

full text
figures and tables
references and citing sentences
relations to other papers

levels run

P abstract

not run

S sections
T body sentences
C citations
R cross-paper relations

Every quoted sentence on this record is the authors'. Every label is from Pith's closed vocabulary, with the probability shown beside it. Every number in the measurements table is the authors', checked by code. Record as JSON

References

Works cited (2)

[1]

Fagin, R., J. Y . Halpern, Y . Moses, and M. Y . Vardi (1995).Reasoning about Knowledge. Cambridge, Mass.: MIT Press. A slightly revised paperback v ersion was published in

View on Pith 1995
[2003]

Halpern, J. Y . and Y . Moses (1992). A guide to completeness an d complexity for modal logics of knowledge and belief. Artiﬁcial Intelligence 54, 319–379. Ladner, R. E. (1977). The computational complexity of prova bility in systems of modal propositional logic. SIAM Journal on Computing 6(3), 467–480. Vardi, M. Y . (1989). On the complexity of epistemic...

View on Pith 1992

Discussion

Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.

[1] [1]

Fagin, R., J. Y . Halpern, Y . Moses, and M. Y . Vardi (1995).Reasoning about Knowledge. Cambridge, Mass.: MIT Press. A slightly revised paperback v ersion was published in

View on Pith 1995

[2] [2003]

Halpern, J. Y . and Y . Moses (1992). A guide to completeness an d complexity for modal logics of knowledge and belief. Artiﬁcial Intelligence 54, 319–379. Ladner, R. E. (1977). The computational complexity of prova bility in systems of modal propositional logic. SIAM Journal on Computing 6(3), 467–480. Vardi, M. Y . (1989). On the complexity of epistemic...

View on Pith 1992