Graded Monads and Behavioural Equivalence Games - Ford, Matthew; Milius, Stefan; Schröder, Lutz; Beohar, Harsh; König, Barbara (Proceedings - Symposium on Logic in Computer Science, 2022)
The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found in 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 infnite variant of such games lead to a novel notion of infnite-depth graded semantics. Under reasonable restrictions, the infnite-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.
CRIS-Team Scopus Importer:2022-09-09
Keywords: Behavioural equivalence; Games; Graded monads; Lineartime/branching-time spectrum; Semantics