paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Relators and Notions of Simulation Revisited

再探 Relator 与模拟概念
LICS 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2025匹配度 1/10 · 论文属于余代数与形式语义中关于 relator、模拟/双模拟闭包性质的理论研究,与用户核心关注的 LLM/Agent 结合静态分析、浮点程序分析、贝叶斯程序分析等方向没有直接关联。引用 1 inbox
Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild
crossref: 2026-09-12

AI 速览

一句话:在余代数框架下系统研究 relator,揭示其与(双)模拟闭包性质、可靠完备性及松弛扩张的对应关系。

模拟与双模拟广泛用于并发系统及模态逻辑;概率、加权、邻域与博弈系统等也需相应概念。通用余代数将系统类型抽象为集合函子,而(双)模拟通过把函子合适扩张到关系上得到,即 relator。本文在最一般意义下研究 relator 及其诱导的(双)相似性:证明保持 1/4-同构拉回的函子可由 coBarr relator 诱导可靠完备的双模拟;建立 relator 性质与闭包性质的等价,表明完整闭包要求 lax extension、可靠性要求保持对角线;证明保持逆像的函子有最大 lax extension。最后将后者用于标记迁移系统,得到高度宽松的新型 twisted bisimulation。

问题
如何以统一方式刻画不同系统类型上的模拟与双模拟概念,并厘清 relator 的性质与其诱导的(双)相似性闭包性质、可靠完备性之间的关系。
方法
在通用余代数框架下,以集合函子及其到关系的扩张(relator)为对象,通过范畴论证明建立函子保持特定拉回/逆像条件与 coBarr relator、lax extension 等性质的联系。
评估
以范畴论定理与等价性证明为主要评估,并通过标记迁移系统的案例研究展示所得最大 lax extension 的应用。
原文摘要(Abstract)

Simulations and bisimulations are ubiquitous in the study of concurrent systems and modal logics of various types. Besides classical relational transition systems, relevant system types include, for instance, probabilistic, weighted, neighbourhood-based, and game-based systems. Universal coalgebra abstracts system types in this sense as set functors. Notions of (bi)simulation then arise by extending the functor to act on relations in a suitable manner, turning it into what may be termed a relator. We contribute to the study of relators in the broadest possible sense, in particular in relation to their induced notions of (bi)similarity. Specifically, (i) we show that every functor that preserves a very restricted type of pullbacks (termed 1/4-iso pullbacks) admits a sound and complete notion of bisimulation induced by the coBarr relator; (ii) we establish equivalences between properties of relators and closure properties of the induced notion of (bi)simulation, showing in particular that the full set of expected closure properties requires the relator to be a lax extension, and that soundness of (bi)simulations requires preservation of diagonals; and (iii) we show that functors preserving inverse images admit a greatest lax extension. In a concluding case study, we apply (iii) to obtain a novel highly permissive notion of twisted bisimulation on labelled transition systems.

链接与引用

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

BibTeX
@inproceedings{paperbot8635,
  title = {Relators and Notions of Simulation Revisited},
  author = {Sergey Goncharov and Dirk Hofmann and Pedro Nora and Lutz Schröder and Paul Wild},
  booktitle = {LICS},
  year = {2025},
  doi = {10.1109/lics65433.2025.00064}
}