一句话:提出从分级单子中提取通用 Spoiler-Duplicator 博弈,统一刻画不同粒度的行为等价,并引入无限深度分级语义。
分级语义框架用分级单子刻画不同粒度(如线性时间/分支时间谱系)的行为等价,并适用于一般系统类型。本文从给定分级单子中提取一个通用的 Spoiler-Duplicator 博弈,该博弈可视为展开等式证明,其实例涵盖模拟与互模拟的标准石子博弈、迹类等价博弈以及余代数行为等价。作者还考虑博弈的无限变体,提出无限深度分级语义的新概念;在合理限制下,将给定分级等价对应的无限深度分级语义刻画为在该等价下的余代数确定化构造。
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 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.