When Are Prime Formulae Characteristic?
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909094765395968 |
|---|---|
| author | Aceto, Luca Della Monica, Dario Fábregas, Ignacio Ingólfsdóttir, Anna |
| author_facet | Aceto, Luca Della Monica, Dario Fábregas, Ignacio Ingólfsdóttir, Anna |
| contents | In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to various behavioural relations in the literature. In particular, characteristic formulae are exactly the prime and consistent ones for all the semantics in van Glabbeek's linear time-branching time spectrum. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_00970 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | When Are Prime Formulae Characteristic? Aceto, Luca Della Monica, Dario Fábregas, Ignacio Ingólfsdóttir, Anna Logic in Computer Science In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to various behavioural relations in the literature. In particular, characteristic formulae are exactly the prime and consistent ones for all the semantics in van Glabbeek's linear time-branching time spectrum. |
| title | When Are Prime Formulae Characteristic? |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2402.00970 |