一句话：系统刻画模态不动点公式可分离性与可定义性在不同模型类上的计算复杂度，并给出分离子构造算法。
论文研究模态不动点公式的模态可分离性：给定 φ 和 φ'，判定是否存在模态公式 ψ 满足 φ⊨ψ 且 ψ⊨¬φ'；其特例为模态可定义性。作者在任意模型、有限模型、树及出度有界模型等类上分析复杂度，主要结果：字（出度≤1）上 PSpace 完全，无限制和二值模型上 ExpTime 完全，出度≤d（d≥3）时有界模型上 TwoExpTime 完全。后一类行为迥异，且模态逻辑在此类上不具 Craig 插值性质。受此启发，作者研究插值项存在性，证明其为 coNExpTime 完全，比有效性更难。论文还给出分离子构造算法，并案例研究分级模态扩展下的分离性。
Modal separability for modal fixpoint formulae is the problem to decide for two given modal fixpoint formulae $φ,φ'$ whether there is a modal formula $ψ$ that separates them, in the sense that $φ\modelsψ$ and $ψ\models\negφ'$. 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2509-24583,
title = {The Complexity of Defining and Separating Fixpoint Formulae in Modal Logic},
author = {Jean Christoph Jung and Jędrzej Kołodziejski},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 3},
year = {2026},
doi = {10.46298/lmcs-22(3:6)2026}
}