Graded Monads and Behavioural Equivalence Games
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2022
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917658548502528 |
|---|---|
| author | Ford, Chase Beohar, Harsh König, Barbara Milius, Stefan Schröder, Lutz |
| author_facet | Ford, Chase Beohar, Harsh König, Barbara Milius, Stefan Schröder, Lutz |
| contents | The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found on the linear-time/branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pebble games for simulation and bisimulation as well as games for trace-like equivalences and coalgebraic behavioural equivalence. Considerations on an infinite variant of such games lead to a novel notion of infinite-depth graded semantics. Under reasonable restrictions, the infinite-depth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2203_15467 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Graded Monads and Behavioural Equivalence Games Ford, Chase Beohar, Harsh König, Barbara Milius, Stefan Schröder, Lutz Logic in Computer Science The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found on the linear-time/branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pebble games for simulation and bisimulation as well as games for trace-like equivalences and coalgebraic behavioural equivalence. Considerations on an infinite variant of such games lead to a novel notion of infinite-depth graded semantics. Under reasonable restrictions, the infinite-depth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand. |
| title | Graded Monads and Behavioural Equivalence Games |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2203.15467 |