Graded Monads and Behavioural Equivalence Games
Chase Ford, Harsh Beohar, Barbara König, Stefan Milius, Lutz Schröder
TL;DR
This work develops a unifying framework for behavioural equivalences across system types by using graded monads to encode depth-parametrized semantics. It derives a generic Spoiler-Duplicator game from a given graded monad, capturing finite-depth and infinite-depth equivalences through pre-determinization in the Eilenberg-Moore setting and a graded determinization construction. The paper shows sound and complete game characterizations for common semantics (bisimilarity, trace, simulation, etc.) and extends to infinite-depth behavior via a final coalgebra perspective, giving a fixpoint view and potential algorithmic approaches. The approach applies across labelled transition and probabilistic systems, linking canonical algebraic structures with coalgebraic semantics to provide a versatile, algebraic view of behavioural equivalence with practical implications for verification and synthesis.
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.