paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity

1-free 正则表达式模互模拟的完备证明系统
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 1/10 · 该论文属于纯进程代数/形式语义领域，研究正则表达式模互模拟的完备证明系统，未涉及 LLM/Agent、静态分析、浮点或贝叶斯程序分析等当前关注方向。虽然与形式化验证有学科上的远亲关系，但研究问题和方法均不在画像核心范围内。引用 16 inbox
Clemens Grabmayer, Wan Fokkink
形式语义逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：为 1-free 正则表达式建立模互模拟的完备证明系统，解决 Milner 开放问题的一个受限情形。

论文研究 Milner 于 1984 年提出的完备性问题：将正则表达式解释为进程，并用 Basic Process Algebra、Kleene 星迭代、死锁 0、成功终止 1 和不动点规则进行公理化时，互模拟等价是否可被完备地证明。尽管完整问题已开放三十余年，本文针对其中 1-free 片段（不含成功终止常量 1）构造了一个完备的证明系统。方法上，作者给出该片段的一组公理与规则，并证明它们相对于互模拟等价既是可靠的也是完备的，即所有互模拟等价的正则表达式都可在系统中推导出。关键结果是解决了该受限情形下的长期开放问题，而含 1 的完整系统仍待研究。

问题
Milner 提出的进程代数中正则表达式互模拟等价的完备公理化问题，在 1-free 片段上能否给出完备证明系统。
方法
构造针对 1-free 正则表达式的公理与推理规则，并证明其相对于互模拟等价的可靠性与完备性。
评估
通过元理论证明（可靠性/完备性定理）评估该证明系统，而非实验；结果显示它完备刻画了该片段的互模拟等价。
原文摘要（Abstract）

Robin Milner (1984) gave a sound proof system for bisimilarity of regular expressions interpreted as processes: Basic Process Algebra with unary Kleene star iteration, deadlock 0, successful termination 1, and a fixed-point rule. He asked whether this system is complete. Despite intensive research over the last 35 years, the problem is still open.

链接与引用

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

BibTeX 
@inproceedings{paperbot5493,
  title = {A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity},
  author = {Clemens Grabmayer and Wan Fokkink},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394744}
}