The Complexity of Deciding Characteristic Formulae Modulo Nested Simulation (extended abstract)
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911159552049152 |
|---|---|
| author | Aceto, Luca Achilleos, Antonis Chalki, Aggeliki Ingólfsdóttir, Anna |
| author_facet | Aceto, Luca Achilleos, Antonis Chalki, Aggeliki Ingólfsdóttir, Anna |
| contents | This paper studies the complexity of determining whether a formula in the modal logics characterizing the nested-simulation semantics is characteristic for some process, which is equivalent to determining whether the formula is satisfiable and prime. The main results are that the problem of determining whether a formula is prime in the modal logic characterizing the 2-nested-simulation preorder is coNP-complete and is PSPACE-complete in the case of the n-nested-simulation preorder, when n>=3. This establishes that deciding characteristic formulae for the n-nested simulation semantics is PSPACE-complete, when n>=3. In the case of the 2-nested simulation semantics, that problem lies in the complexity class DP, which consists of languages that can be expressed as the intersection of one language in NP and of one in coNP. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_14089 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Complexity of Deciding Characteristic Formulae Modulo Nested Simulation (extended abstract) Aceto, Luca Achilleos, Antonis Chalki, Aggeliki Ingólfsdóttir, Anna Logic in Computer Science This paper studies the complexity of determining whether a formula in the modal logics characterizing the nested-simulation semantics is characteristic for some process, which is equivalent to determining whether the formula is satisfiable and prime. The main results are that the problem of determining whether a formula is prime in the modal logic characterizing the 2-nested-simulation preorder is coNP-complete and is PSPACE-complete in the case of the n-nested-simulation preorder, when n>=3. This establishes that deciding characteristic formulae for the n-nested simulation semantics is PSPACE-complete, when n>=3. In the case of the 2-nested simulation semantics, that problem lies in the complexity class DP, which consists of languages that can be expressed as the intersection of one language in NP and of one in coNP. |
| title | The Complexity of Deciding Characteristic Formulae Modulo Nested Simulation (extended abstract) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2509.14089 |