Complexity results for modal logic with recursion via translations and tableaux

TL;DR

The paper investigates the complexity of multi-modal logics with recursion under frame restrictions by leveraging translations to and from the μ-calculus and by constructing Kozen-style tableau systems. It shows how translations can transfer known EXP/PSPACE bounds, yields finite-model properties in many cases, and provides tableau-based termination criteria to obtain PSPACE and, in broad terms, $2^{\mathsf{EXP}}$-level upper bounds. The authors also develop a uniform tableau-to-μ-calculus translation to handle logics without and with negative introspection, delivering a cohesive, method-driven framework for complexity analysis and satisfiability testing. The work identifies tight bounds in several single- and multi-agent settings (notably PSPACE for $K4^{\mu}$-type logics and EXP bounds in others) and leaves open precise results for certain symmetric/euclidean and combined cases, guiding future investigations. Overall, the paper advances a systematic, translatable approach to complexity in recursive modal logics with restricted frames, with substantial implications for decision procedures and finite-model reasoning in epistemic settings.

Abstract

This paper studies the complexity of classical modal logics and of their extension with fixed-point operators, using translations to transfer results across logics. In particular, we show several complexity results for multi-agent logics via translations to and from the $μ$-calculus and modal logic, which allow us to transfer known upper and lower bounds. We also use these translations to introduce terminating and non-terminating tableau systems for the logics we study, based on Kozen's tableau for the $μ$-calculus and the one of Fitting and Massacci for modal logic. Finally, we describe these tableaux with $μ$-calculus formulas, thus reducing the satisfiability of each of these logics to the satisfiability of the $μ$-calculus, resulting in a general 2EXP upper bound for satisfiability testing.

Figures (7)

• Figure 1: The frame-property-preservation graph
• Figure 2: An example where the use of the alternative axiom for symmetricity would yield an incorrect translation.
• Figure 3: The new model, based on a state $s$ in $\mathcal{M}$, with two neighbours $t_1,t_2$.
• Figure 4: Tableaux for $\varphi_1$ and $\varphi_2$. The dots represent that the tableau keeps repeating as from the identical node above. The x mark represents a propositionally closed branch.
• Figure 5: A finite $\xrightarrow{X}$-path from $\sigma~\psi_1$ to $\sigma~\psi_2$ may visit other tableau prefixes, and an infinite $\xrightarrow{X}$-path from $\sigma~\psi_1$ may include finite segments that visit other prefixes, before continuing with an infinite path from a formula $\psi_2$. Each square area represents a tableau prefix, or a graph $g \in G^t$. For $S$ the set of pairs of formulas that appear near the bottom, the left figure illustrates the relation $(\psi_1,\psi_2) \xrightarrow{g} S$ and the right one the relation $\psi_1 \xrightarrow{g} S, \psi_2$ (Definition \ref{['def:searchTtoS']}).

Theorems & Definitions (88)

• Definition 2.1
• Example 2.2
• Definition 2.3: Bisimulation
• Theorem 2.4: Hennessy-Milner Theorem hennessy1985algebraicmu_calc_model_checkhandbook_model_check
• Theorem 2.5: ladnermodcompHalpern2007CharacterizingRybakovShkatovBCompDagostino2013S5
• Theorem 2.6: Halpern1992
• Remark 2.7
• Theorem 2.8: Kozen1983
• Theorem 2.9: emerson2001model
• Theorem 2.10