Relating Apartness and Branching Bisimulation Games
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_ | 1866909377911324672 |
|---|---|
| author | Rot, Jurriaan Junges, Sebastian Beohar, Harsh |
| author_facet | Rot, Jurriaan Junges, Sebastian Beohar, Harsh |
| contents | Geuvers and Jacobs (LMCS 2021) formulated the notion of apartness relation on state-based systems modelled as coalgebras. In this context apartness is formally dual to bisimilarity, and gives an explicit proof system for showing that certain states are not bisimilar. In the current paper, we relate apartness to another classical element of the theory of behavioural equivalences: that of turn-based two-player games. Studying both strong and branching bisimilarity, we show that winning configurations for the Spoiler player correspond to apartness proofs, for transition systems that are image-finite (in the case of strong bisimilarity) and finite (in the case of branching bisimilarity). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_02977 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Relating Apartness and Branching Bisimulation Games Rot, Jurriaan Junges, Sebastian Beohar, Harsh Logic in Computer Science Geuvers and Jacobs (LMCS 2021) formulated the notion of apartness relation on state-based systems modelled as coalgebras. In this context apartness is formally dual to bisimilarity, and gives an explicit proof system for showing that certain states are not bisimilar. In the current paper, we relate apartness to another classical element of the theory of behavioural equivalences: that of turn-based two-player games. Studying both strong and branching bisimilarity, we show that winning configurations for the Spoiler player correspond to apartness proofs, for transition systems that are image-finite (in the case of strong bisimilarity) and finite (in the case of branching bisimilarity). |
| title | Relating Apartness and Branching Bisimulation Games |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2411.02977 |