paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Graded Monads and Behavioural Equivalence Games

分级单子与行为等价博弈
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 2/10 · 论文属于形式语义与余代数理论,研究分级单子、行为等价博弈与无限深度分级语义,未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,与画像核心方向关联较弱。引用 15 inbox
Chase Ford, Stefan Milius, Lutz Schröder, Harsh Beohar, Barbara König
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:提出从分级单子中提取通用 Spoiler-Duplicator 博弈,统一刻画不同粒度的行为等价,并引入无限深度分级语义。

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

问题
如何为分级语义提供一个统一、通用的行为等价博弈,并刻画不同粒度的等价(包括线性时间/分支时间)以及无限深度情形?
方法
从给定的分级单子中通用地提取 Spoiler-Duplicator 博弈,将其解释为等式证明的展开;并研究该博弈的无限变体,通过余代数确定化来刻画无限深度分级语义。
评估
论文以理论构造和实例覆盖进行评估:展示标准模拟、互模拟、迹类等价与余代数行为等价等作为该通用博弈的实例,并在限制条件下证明无限深度分级语义的确定化特征。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{FordMSB022,
  title = {Graded Monads and Behavioural Equivalence Games},
  author = {Chase Ford and Stefan Milius and Lutz Schröder and Harsh Beohar and Barbara König},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3533374}
}