Deciding characteristic formulae: A journey in the branching-time spectrum
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911545547554816 |
|---|---|
| author | Aceto, Luca Achilleos, Antonis Chalki, Aggeliki Ingolfsdottir, Anna |
| author_facet | Aceto, Luca Achilleos, Antonis Chalki, Aggeliki Ingolfsdottir, Anna |
| contents | Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence or preorder checking to model checking, and are exactly the formulae in the modal logics characterizing classic behavioural equivalences and preorders for which model checking can be reduced to equivalence or preorder checking.
This paper studies the complexity of determining whether a formula is characteristic for some process in each of the logics providing modal characterizations of the simulation-based semantics in van Glabbeek's branching-time spectrum. Since characteristic formulae in each of those logics are exactly the satisfiable and prime ones, this article presents complexity results for the satisfiability and primality problems, and investigates the boundary between modal logics for which those problems can be solved in polynomial time and those for which they become (co)NP- or PSPACE-complete. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_22277 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Deciding characteristic formulae: A journey in the branching-time spectrum Aceto, Luca Achilleos, Antonis Chalki, Aggeliki Ingolfsdottir, Anna Logic in Computer Science Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence or preorder checking to model checking, and are exactly the formulae in the modal logics characterizing classic behavioural equivalences and preorders for which model checking can be reduced to equivalence or preorder checking. This paper studies the complexity of determining whether a formula is characteristic for some process in each of the logics providing modal characterizations of the simulation-based semantics in van Glabbeek's branching-time spectrum. Since characteristic formulae in each of those logics are exactly the satisfiable and prime ones, this article presents complexity results for the satisfiability and primality problems, and investigates the boundary between modal logics for which those problems can be solved in polynomial time and those for which they become (co)NP- or PSPACE-complete. |
| title | Deciding characteristic formulae: A journey in the branching-time spectrum |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2505.22277 |