Modal Separability of Fixpoint Formulae
Jean Christoph Jung, Jędrzej Kołodziejski
TL;DR
This work addresses the problem of modal separability for formulae in the modal mu-calculus: given two mutually exclusive $\mu\mathsf{ML}$-formulae $\varphi$ and $\varphi'$, it asks whether there exists a modal separator $\psi\in\mathsf{ML}$ such that $\varphi\models\psi\models\neg\varphi'$. The authors develop a model-theoretic characterization via bisimulations and leverage automata-theoretic tools (nondeterministic parity tree automata) to obtain tight complexity bounds and constructive procedures for separators, including the notion of $n$-uniform consequences to bound modal depth and to synthesize separators of optimal size. They prove $\mathsf{EXPTIME}$-complete separability for arbitrary models and $PSPACE$-complete separability over words, with separators computable in doubly-exponential time (arbitrary models) or exponential time (word case); in the word setting, separators have exponential size, while in general they may be doubly exponential, reflecting a succinctness gap between $\mu\mathsf{ML}$ and $\mathsf{ML}$. The results extend to finitely branching and finite trees, and they discuss ontological extensions, uniform interpolation, and the tightness of these bounds, while also presenting a divide-and-conquer construction that yields efficient word-case separators and establishing exponential succinctness gaps in that domain as well.
Abstract
We study modal separability for fixpoint formulae: given two mutually exclusive fixpoint formulae $\varphi,\varphi'$, decide whether there is a modal formula $ψ$ that separates them, that is, that satisfies $\varphi\modelsψ\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.