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.

翻译：分级语义框架利用分级单子捕捉不同粒度下的行为等价关系，例如线性时间/分支时间谱系中的行为等价，适用于通用系统类型。我们描述了一种针对分级语义的通用施普雷-杜普利卡特博弈，该博弈从给定分级单子中提取，可视为等式证明的展开过程；其特例包括用于仿真和互模拟的标准石子博弈，以及用于迹类等价与余代数行为等价的博弈。对此类博弈无限变体的考量引出了无限深度分级语义的新概念。在合理约束条件下，与给定分级等价相关的无限深度分级语义可通过该等价下余代数的确定性化构造来刻画。