Modal Separability of Fixpoint Formulae
Jean Christoph Jung, J\k{e}drzej Ko{\l}odziejski
TL;DR
This paper investigates the complexity of modal separability for fixpoint formulae, providing tight bounds and optimal algorithms for deciding and computing separators across various structures.
Contribution
It establishes tight complexity bounds and optimal algorithms for deciding and computing modal separators for fixpoint formulae in different settings.
Findings
EXPTIME-complete in general
PSPACE-complete over words
Separators computable in doubly exponential and exponential time
Abstract
We study modal separability for fixpoint formulae: given two mutually exclusive fixpoint formulae , decide whether there is a modal formula that separates them, that is, that satisfies . 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Control Systems Optimization