Proving Behavioural Apartness
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911853264764928 |
|---|---|
| author | Turkenburg, Ruben Beohar, Harsh Kupke, Clemens Rot, Jurriaan |
| author_facet | Turkenburg, Ruben Beohar, Harsh Kupke, Clemens Rot, Jurriaan |
| contents | Bisimilarity is a central notion for coalgebras. In recent work, Geuvers and Jacobs suggest to focus on apartness, which they define by dualising coalgebraic bisimulations. This yields the possibility of finite proofs of distinguishability for a wide variety of state-based systems.
We propose behavioural apartness, defined by dualising behavioural equivalence rather than bisimulations. A motivating example is the subdistribution functor, where the proof system based on bisimilarity requires an infinite quantification over couplings, whereas behavioural apartness instantiates to a finite rule. In addition, we provide optimised proof rules for behavioural apartness and show their use in several examples. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_16588 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Proving Behavioural Apartness Turkenburg, Ruben Beohar, Harsh Kupke, Clemens Rot, Jurriaan Logic in Computer Science Bisimilarity is a central notion for coalgebras. In recent work, Geuvers and Jacobs suggest to focus on apartness, which they define by dualising coalgebraic bisimulations. This yields the possibility of finite proofs of distinguishability for a wide variety of state-based systems. We propose behavioural apartness, defined by dualising behavioural equivalence rather than bisimulations. A motivating example is the subdistribution functor, where the proof system based on bisimilarity requires an infinite quantification over couplings, whereas behavioural apartness instantiates to a finite rule. In addition, we provide optimised proof rules for behavioural apartness and show their use in several examples. |
| title | Proving Behavioural Apartness |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2404.16588 |