Intuitionistic implication makes model checking hard

TL;DR

This paper analyzes the computational complexity of model checking in various intuitionistic and modal propositional logics, revealing that it is generally P-complete even for simple fragments, with some cases in LOGCFL.

Contribution

It establishes the P-completeness of model checking for implicational fragments of several intuitionistic and modal logics, and explores how additional connectives and variables affect complexity.

Findings

Model checking is P-complete for implicational fragments of intuitionistic and modal logics.

For BPL and FPL, model checking remains P-hard even with a single variable.

Variable-free formulas outside implicational fragments have model checking in LOGCFL.

Abstract

We investigate the complexity of the model checking problem for intuitionistic and modal propositional logics over transitive Kripke models. More specific, we consider intuitionistic logic IPC, basic propositional logic BPL, formal propositional logic FPL, and Jankov's logic KC. We show that the model checking problem is P-complete for the implicational fragments of all these intuitionistic logics. For BPL and FPL we reach P-hardness even on the implicational fragment with only one variable. The same hardness results are obtained for the strictly implicational fragments of their modal companions. Moreover, we investigate whether formulas with less variables and additional connectives make model checking easier. Whereas for variable free formulas outside of the implicational fragment, FPL model checking is shown to be in LOGCFL, the problem remains P-complete for BPL.