Parameterized complexity of n-dense modal logics

1. Problem Statement

The paper addresses the computational complexity of the satisfiability problem for a specific class of normal modal logics known as $n$-dense logics ($KDe(n)$).

• Definition: These logics are characterized by the axiom $\Box^n p \to \Box p$ (where $n > 1$). Semantically, their Kripke frames satisfy the property $R \subseteq R^n$, meaning that if there is an edge between two nodes, there must exist a path of length $n$ between them.
• Existing Knowledge:
  • The satisfiability problem for these logics is known to be in NEXPTIME (via filtration techniques).
  • It is known to be PSPACE-hard.
  • The exact tight bound is an open problem, suspected to lie somewhere between PSPACE and EXPSPACE.
• The Gap: Standard filtration techniques produce models with exponentially many nodes independent of the formula's modal depth, making it difficult to prove membership in lower complexity classes like PSPACE or parameterized classes.
• Goal: To refine the complexity analysis using parameterized complexity theory. Specifically, the author aims to prove that the problem belongs to para-PSPACE when the modal depth ($d(\phi)$) of the input formula is treated as a parameter.

2. Methodology

The author employs a Tableau Calculus approach, enhanced by a novel structural analysis tool called Recursive Windows.

A. Tableau Calculus

The paper utilizes a semantic tableau method where the goal is to construct a model (or prove none exists) by expanding a set of formulas.

• Classical Consistent Saturation (CCS): The algorithm operates on sets of formulas that are classically consistent and saturated (closed under classical logical consequences).
• The Challenge: In $n$-dense logics, satisfying a formula $\neg \Box \phi$ requires creating a successor world. However, the density axiom ($R \subseteq R^n$) forces the insertion of $n-1$ intermediate nodes between any two connected worlds. A naive tableau construction leads to infinite or exponentially large structures.

B. The Concept of "Windows"

To manage the infinite nature of the models, the paper generalizes the "window" technique introduced in previous work (Balbiani & Gasquet) to a recursive setting.

• Definition of a Window: A window is a finite, polynomial-sized structure representing a "slice" of the infinite tableau.
  • A $(k, n, \lambda)$-window for a pair of CCS sets $(u, v_0)$ consists of a sequence of nodes (CCS sets) and a sequence of sub-windows.
  • The parameter $k$ represents the nesting depth (related to modal depth). As $k$ decreases, the window handles formulas with lower modal depth.
  • The length of the window sequence is determined by a function $\chi(u)$, which is exponential in the size of the input but depends on the modal depth.
• Recursive Structure: A window contains sub-windows for the relationships between its nodes. This allows the algorithm to reason about the infinite chain of intermediate nodes required by the density axiom without explicitly constructing the entire chain.
• Continuations and Loop Detection: The algorithm relies on the concept of $k$-continuations. If a sequence of windows is long enough (specifically, longer than the number of possible distinct windows, which is bounded by $2^{P(|u|)}$), a repetition must occur.
  • If a window $W_2$ is a continuation of $W_1$, and the sequence repeats, the algorithm can infer that the model can be extended infinitely (or cyclically) without contradiction.
  • This allows the algorithm to terminate by detecting loops rather than exploring the infinite depth.

C. The Algorithm

The proposed algorithm, Sat, decides satisfiability for $KDe(2)$ (the 2-dense case) and is generalized for $KDe(n)$.

1. Input: A set of formulas $s$.
2. Process:
   • Select a Classically Consistent Saturation (CCS) $u$ from $s$.
   • For every $\neg \Box \phi \in u$, non-deterministically pick a successor CCS $v_0$.
   • Construct a window $W$ of length $\chi(u)$ starting with $(u, v_0)$.
   • Recursively verify the satisfiability of the window's nodes and its sub-windows.
   • Use continuation checks to detect if the sequence of windows repeats. If a repetition is found, the branch is considered satisfiable (loop detection).
3. Termination: The recursion depth is bounded by the modal depth $d(u)$, and the window length is bounded by a function of the formula size and modal depth.

3. Key Contributions

1. Generalization of Windows: The paper introduces Recursive Windows, extending the non-recursive window technique to handle the complex, nested dependencies required by $n$-dense logics.
2. Algorithm Design: It designs a specific tableau-based decision procedure that operates by exploring small, polynomial-sized "windows" of the model rather than the full infinite model.
3. Complexity Classification: It proves that the satisfiability problem for $n$-dense logics is in para-PSPACE.
   • Parameter: The modal depth of the input formula, $d(\phi)$.
   • Complexity: The space complexity is $O(|\phi|^3 \cdot 2^{d(\phi)^5})$. Since $d(\phi)$ is the parameter $\kappa$, the space is $f(\kappa) \cdot poly(|\phi|)$, satisfying the definition of para-PSPACE.
4. Hardness Proof: It reaffirms that $n$-dense satisfiability is PSPACE-hard, establishing that the problem is at least as hard as standard PSPACE problems.

4. Results

• Membership: The main result is Corollary 9.1: For all $n \in \mathbb{N}$, $KDe(n)$-satisfiability is in para-PSPACE.
• Space Complexity Analysis:
  • The algorithm requires space proportional to $O(|u|^3 \cdot 2^{d(u)^5})$.
  • The proof involves analyzing the memory cost of the recursive SatW function, showing that the stack depth is bounded by the modal depth and the width of the search is bounded by the number of distinct windows (which is exponential in the formula size but polynomial in the parameter).
• Correctness: The paper provides rigorous proofs for:
  • Soundness: If the algorithm returns True, a model exists (Lemma 8.2).
  • Completeness: If a model exists, the algorithm returns True (Lemma 8.3). This is achieved by constructing a model from the successful execution trace of the algorithm, merging disjoint models via the window structure.

5. Significance

• Refining Complexity Bounds: This work moves beyond the coarse NEXPTIME upper bound for $n$-dense logics. By utilizing parameterized complexity, it demonstrates that the "hardness" of these logics is tightly coupled to the modal depth of the formulas. For formulas with small modal depth (common in practical applications), the problem is significantly more tractable (polynomial space) than the general worst-case suggests.
• Methodological Innovation: The introduction of recursive windows provides a powerful new tool for analyzing modal logics with complex frame properties (like density). It offers a way to handle infinite structures in finite space by leveraging the periodicity of the tableau expansion.
• Broader Applicability: The author suggests that this technique could be extended to other open problems in modal logic, particularly those involving intermediate worlds or multimodal extensions, where traditional filtration methods fail to provide tight complexity bounds.
• Field Impact: The paper highlights that parameterized complexity has been underutilized in modal logic research and argues for its adoption to better understand the tractability of high-complexity logical systems.

In summary, Gasquet successfully bridges the gap between the theoretical hardness of $n$-dense logics and practical tractability by showing that fixing the modal depth reduces the problem to a polynomial-space computation, utilizing a sophisticated recursive window mechanism to manage the infinite nature of dense Kripke frames.