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.

翻译：模态不动点公式的模态可分离性问题是：对于给定的两个模态不动点公式 $\varphi,\varphi'$，判断是否存在一个模态公式 $ψ$ 能够分离它们，即满足 $\varphi\modelsψ$ 且 $ψ\models\neg\varphi'$。我们研究了模态可分离性及其特例模态可定义性在各类模型上的表现，包括任意模型、有限模型、树结构以及出度有界模型。我们的主要结果表明：在字模型（即出度 $\leq 1$ 的模型）上，模态可分离性是 PSpace 完全的；在无限制模型及二元模型上是 ExpTime 完全的；在出度受限于某个 $d\geq 3$ 的模型上则是 TwoExpTime 完全的。值得注意的是，后一种情况在本质上与其他情况不同，模态逻辑在此类模型上不满足 Craig 插值性质。受此启发，我们还研究了作为模态可分离性特例的插值存在性问题，并证明该问题是 coNExpTime 完全的，因而比逻辑有效性判定更为困难。除了判定可分离性，我们还提供了构造分离子的有效算法。最后，我们通过案例研究探讨了带分级模态词的模态不动点公式扩展，并分析了其与模态公式及分级模态公式的可分离性。