Conformance Games for Graded Semantics
Jonas Forster, Lutz Schröder, Paul Wild
TL;DR
The paper develops a generic, game-theoretic account of behavioural conformances by extending graded semantics to topological categories, enabling coarsened comparisons beyond equivalence. It defines finite-depth and infinite-depth conformance games parametrized by system type functors and graded monads, and proves soundness/completeness results linking winning strategies to conformance relations via pre-determinization. The framework is instantiated to trace inclusion, probabilistic trace distance, and bisimulation topologies, and is further enriched with a syntactic relational-algebraic presentation and concrete examples, including metric and nondeterministic settings. This approach provides a unifying, coalgebraic foundation for a wide spectrum of linear-time/branching-time conformance notions, with potential for algorithmic strategy synthesis and witness extraction in practical verification tasks.
Abstract
Game-theoretic characterizations of process equivalences traditionally form a central topic in concurrency; for example, most equivalences on the classical linear-time / branching-time spectrum come with such characterizations. Recent work on so-called graded semantics has led to a generic behavioural equivalence game that covers the mentioned games on the linear-time~/ branching-time spectrum and moreover applies in coalgebraic generality, and thus instantiates also to equivalence games on systems with non-relational branching type (probabilistic, weighted, game-based etc.). In the present work, we generalize this approach to cover other types of process comparison beyond equivalence, such as behavioural preorders or pseudometrics. At the most general level, we abstract such notions of behavoiural conformance in terms of topological categories, and later specialize to conformances presented as relational structures to obtain a concrete syntax. We obtain a sound and complete generic game for behavioural conformances in this sense. We present a number of instantiations, obtaining game characterizations of, e.g., trace inclusion, probabilistic trace distance, bisimulation topologies, and simulation distances on metric labelled transition systems.