分级单子与行为等价博弈
Graded Monads and Behavioural Equivalence Games
AI总结：
本文从分级单子中提取通用 Spoiler-Duplicator 博弈以刻画分级语义，并提出无穷深度分级语义，证明其可由余代数确定化构造刻画。
摘要：
分级语义框架利用分级单子来刻画不同粒度的行为等价，例如在线性时间/分支时间谱上以及一般系统类型中所见的行为等价。我们描述了一种用于分级语义的通用 Spoiler-Duplicator 博弈，该博弈从给定的分级单子中提取，并可被视为展开一个等式证明；实例包括用于模拟和互模拟的标准 pebble 博弈，以及用于迹类等价和余代数行为等价的博弈。对这类博弈的无穷变体的考虑引出了无穷深度分级语义这一新概念。在合理限制下，与给定分级等价相关联的无穷深度分级语义可以通过在所讨论等价下的余代数确定化构造来刻画。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
