Graded Monads and Behavioural Equivalence Games
Abstract
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.
Keywords
Cite
@article{arxiv.2203.15467,
title = {Graded Monads and Behavioural Equivalence Games},
author = {Chase Ford and Harsh Beohar and Barbara König and Stefan Milius and Lutz Schröder},
journal= {arXiv preprint arXiv:2203.15467},
year = {2024}
}