paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Quasi-Open Bisimilarity with Mismatch is Intuitionistic

带 mismatch 的准开放互模拟是直觉主义的
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 1/10 · 该论文研究π演算中准开放互模拟与mismatch的扩展、开放barbed互模拟一致性及直觉主义模态逻辑刻画，属于并发理论/形式语义，与用户核心方向（面向ML/Agentic程序的静态分析、LLM与静态分析/形式化验证交叉、浮点或贝叶斯程序分析）没有直接交集。其Abella机械化虽与定理证明工程边缘相关，但整体匹配度很低。引用 15 inbox
Ross Horne, Ki Yung Ahn, Shang-wei Lin, Alwen Tiu
形式语义并发、并行与内存模型定理证明与证明工程
crossref: 2026-09-12

AI 速览

一句话：将准开放互模拟扩展到含 mismatch 的 π-演算，证明其与开放 barbed 互模拟一致，并有直觉主义模态逻辑刻画。

准开放互模拟是 π-演算中保证同余的最粗互模拟之一；将其扩展以处理 mismatch 守卫（不等式）并非显然，因为需要为名称不等提供构造性证据。本文提出准开放互模拟的最小扩展：允许制造新名以见证不等式，并证明该扩展具有典范性和稳健性，与开放 barbed 互模拟重合，且可由一种既有模态逻辑的直觉主义变体刻画。作者还分析更著名的开放互模拟，确定其处理 mismatch 的最粗扩展。文中给出隐私性质检查的应用，并使用证明助手 Abella 机器化验证示例与可靠性结果。

问题
如何将 π-演算的准开放互模拟扩展到含 mismatch（不等守卫）的情形，并保持同余性、最粗性与逻辑刻画？
方法
通过允许制造新名作为不等式成立的构造性证据，给出准开放互模拟的最小扩展，并与开放 barbed 互模拟及直觉主义模态逻辑变体建立对应；同时用 Abella 机器化验证。
评估
通过同余性、典范性、与开放 barbed 互模拟重合及直觉主义模态逻辑刻画等理论结果进行评估，并在 Abella 中机器化验证示例与可靠性，同时讨论隐私性质检查应用。
原文摘要（Abstract）

Quasi-open bisimilarity is the coarsest notion of bisimilarity for the π-calculus that is also a congruence. This work extends quasi-open bisimilarity to handle mismatch (guards with inequalities). This minimal extension of quasi-open bisimilarity allows fresh names to be manufactured to provide constructive evidence that an inequality holds. The extension of quasi-open bisimilarity is canonical and robust --- coinciding with open barbed bisimilarity (an objective notion of bisimilarity congruence) and characterised by an intuitionistic variant of an established modal logic. The more famous open bisimilarity is also considered, for which the coarsest extension for handling mismatch is identified. Applications to checking privacy properties are highlighted. Examples and soundness results are mechanised using the proof assistant Abella.

链接与引用

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

BibTeX 
@inproceedings{paperbot4323,
  title = {Quasi-Open Bisimilarity with Mismatch is Intuitionistic},
  author = {Ross Horne and Ki Yung Ahn and Shang-wei Lin and Alwen Tiu},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209125}
}