paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Rooted Divergence-Preserving Branching Bisimilarity is a Congruence

有根发散保持分支互模拟是同余关系
LMCS vol.Volume 16, Issue 32020匹配度 1/10 · 论文研究进程代数中“有根发散保持分支互模拟”的同余性，属于纯形式语义/并发理论；与用户关注的 LLM/Agent 用于程序分析、浮点程序分析、贝叶斯程序分析以及静态分析工具落地均无直接关联。引用 4 inbox
Rob van Glabbeek, Bas Luttik, Linda Spaninks
形式语义并发、并行与内存模型
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：证明在由 nil、动作前缀、选择与递归构成的过程语言中，有根发散保持分支互模拟是同余关系。

本文研究进程规范语言中行为等价关系的同余性质，关注有根发散保持分支互模拟（rooted divergence-preserving branching bisimilarity）。该语言由 nil、动作前缀、选择和递归构造组成。论文证明，这一等价关系在该语言的所有语法构造下都保持：若两个进程等价，则把它们放入相同的上下文后仍等价。因此有根发散保持分支互模拟构成同余关系，可用于组合式地推理此类进程规范。论文为纯理论证明，未涉及实现或实验评估。

问题
有根发散保持分支互模拟在包含 nil、动作前缀、选择和递归的过程规范语言中是否对语言构造构成同余关系？
方法
通过数学证明，论证该等价关系被 nil、动作前缀、选择和递归这些构造保持。
评估
以定理证明形式给出结果，证明有根发散保持分支互模拟是该语言的同余；未报告实验或工具评估。
原文摘要（Abstract）

We prove that rooted divergence-preserving branching bisimilarity is a congruence for the process specification language consisting of nil, action prefix, choice, and the recursion construct.

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@article{abs-1801-01180,
  title = {Rooted Divergence-Preserving Branching Bisimilarity is a Congruence},
  author = {Rob van Glabbeek and Bas Luttik and Linda Spaninks},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 16, Issue 3},
  year = {2020},
  doi = {10.23638/lmcs-16(3:14)2020}
}