Modal Separability of Fixpoint Formulae
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866913375369297920 |
|---|---|
| author | Jung, Jean Christoph Kołodziejski, Jędrzej |
| author_facet | Jung, Jean Christoph Kołodziejski, Jędrzej |
| contents | 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 $φ\modelsψ\models\negφ'$. 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_01497 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Modal Separability of Fixpoint Formulae Jung, Jean Christoph Kołodziejski, Jędrzej Logic in Computer Science 03B70 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 $φ\modelsψ\models\negφ'$. 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. |
| title | Modal Separability of Fixpoint Formulae |
| topic | Logic in Computer Science 03B70 |
| url | https://arxiv.org/abs/2406.01497 |