The Complexity of Defining and Separating Fixpoint Formulae in Modal Logic

TL;DR

This work provides a comprehensive automata-theoretic analysis of modal separability and definability for the modal $\mu$-calculus across several model classes, revealing a nuanced complexity landscape: $\mathsf{PSPACE}$-complete over words, $\text{ExpTime}$-complete over unrestricted and binary models, and a sharp jump to $\text{TwoExpTime}$-hardness for ternary and higher-arity trees. It establishes foundational model-theoretic characterizations via joint consistency and bisimulation quotients, and develops effective procedures to construct separators when they exist. A key insight is that modal separability can be strictly harder than definability, especially in higher-arity tree classes where Craig interpolation fails. The paper also demonstrates how graded modalities interact with separability, showing distinct complexity profiles depending on whether grades appear in the separator. Overall, the results provide both tight complexity boundaries and practical automata-based methods for deciding and constructing separators, with a rich set of directions for further study in interpolation, graded logics, and related decision problems.

Abstract

Modal separability for modal fixpoint formulae is the problem to decide for two given modal fixpoint formulae $\varphi,\varphi'$ whether there is a modal formula $ψ$ that separates them, in the sense that $\varphi\modelsψ$ and $ψ\models\neg\varphi'$. We study modal separability and its special case modal definability over various classes of models, such as arbitrary models, finite models, trees, and models of bounded outdegree. Our main results are that modal separability is PSpace-complete over words, that is, models of outdegree $\leq 1$, ExpTime-complete over unrestricted and over binary models, and TwoExpTime-complete over models of outdegree bounded by some $d\geq 3$. Interestingly, this latter case behaves fundamentally different from the other cases also in that modal logic does not enjoy the Craig interpolation property over this class. Motivated by this we study also the induced interpolant existence problem as a special case of modal separability, and show that it is coNExpTime-complete and thus harder than validity in the logic. Besides deciding separability, we also provide algorithms for the effective construction of separators. Finally, we consider in a case study the extension of modal fixpoint formulae by graded modalities and investigate separability by modal formulae and graded modal formulae.

Figures (2)

• Figure 1: Witness of joint consistency: dashed lines and colors indicate the $\{a\}$-bisimulation.
• Figure 2: Model of a computation tree of $\mathbb{A}\xspace$, enforced by formula $\chi$.

Theorems & Definitions (61)

• Example 1.1
• Theorem 2.1
• Definition 3.1
• Example 3.2
• Example 3.3
• Lemma 3.4
• proof
• Theorem 3.5
• Lemma 3.6
• proof