We study modal separability for fixpoint formulae: given two mutually exclusive fixpoint formulae $\varphi,\varphi'$, decide whether there is a modal formula $\psi$ that separates them, that is, that satisfies $\varphi\models\psi\models\neg\varphi'$. This problem has applications for finding simple reasons for inconsistency. Our main contributions are tight complexity bounds for deciding modal separability and optimal ways to compute a separator if it exists. More precisely, it is EXPTIME-complete in general and PSPACE-complete over words. Separators can be computed in doubly exponential time in general and in exponential time over words, and this is optimal as well. The results for general structures transfer to arbitrary, finitely branching, and finite trees. The word case results hold for finite, infinite, and arbitrary words.

翻译：我们研究不动点公式的模态可分离性问题：给定两个互斥的不动点公式 $\varphi,\varphi'$，判定是否存在一个模态公式 $\psi$ 能将它们分离，即满足 $\varphi\models\psi\models\neg\varphi'$。该问题在寻找不一致性的简单原因方面具有应用价值。我们的主要贡献在于给出了判定模态可分离性的严格复杂度界限，以及存在分离子时计算该分离子的最优方法。具体而言，该问题在一般情况下是 EXPTIME 完全的，在字结构上是 PSPACE 完全的。分离子可在一般情况下以双指数时间计算，在字结构上以指数时间计算，且这两种时间复杂度均是最优的。一般结构上的结果可推广至任意树、有限分支树和有限树。字结构上的结果适用于有限字、无限字及任意字。