A meta-modal logic for bisimulations
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_ | 1866915930634715136 |
|---|---|
| author | Burrieza, Alfredo Soler-Toscano, Fernando Yuste-Ginel, Antonio |
| author_facet | Burrieza, Alfredo Soler-Toscano, Fernando Yuste-Ginel, Antonio |
| contents | We propose a modal study of the notion of bisimulation. Our contribution is threefold. First, we extend the basic modal language with a new modality $\nbi$, whose intended meaning is universal quantification over all states that are bisimilar to the current one. We show that bisimulations are definable in this object language via frame correspondence. Second, we provide a sound and complete axiomatisation of the class of all pairs of Kripke models that are bisimulation-related. Third, we show that the satisfiability problem of our logic is decidable and PSPACE-complete via a translation to standard modal logic $K$ under a simple frame condition. All our results are encoded and verified by Isabelle/HOL. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_15117 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A meta-modal logic for bisimulations Burrieza, Alfredo Soler-Toscano, Fernando Yuste-Ginel, Antonio Logic in Computer Science Logic 03B45 F.4.0 We propose a modal study of the notion of bisimulation. Our contribution is threefold. First, we extend the basic modal language with a new modality $\nbi$, whose intended meaning is universal quantification over all states that are bisimilar to the current one. We show that bisimulations are definable in this object language via frame correspondence. Second, we provide a sound and complete axiomatisation of the class of all pairs of Kripke models that are bisimulation-related. Third, we show that the satisfiability problem of our logic is decidable and PSPACE-complete via a translation to standard modal logic $K$ under a simple frame condition. All our results are encoded and verified by Isabelle/HOL. |
| title | A meta-modal logic for bisimulations |
| topic | Logic in Computer Science Logic 03B45 F.4.0 |
| url | https://arxiv.org/abs/2507.15117 |