Milner 正则表达模互模拟证明系统完备（结晶：正则表达进程图解释的近坍缩）
计算机科学中的逻辑
2022-11-10 v2 形式语言与自动机理论
摘要
Milner（1984）为正则表达式定义了进程语义。他给出了一个用于正则表达式进程解释互模拟的可靠证明系统，并问及该系统是否完备。我们概念性地报告了一个证明，通过动机说明、举例阐释与描述所有主要步骤来展示 Milner 系统是完备的。我们大幅精炼了 Grabmayer 与 Fokkink（2020）针对 Milner 系统限于“无 1”正则表达式的完备性证明。作为一个关键难点，我们认识到带有空步转移且满足分层环存在/消除性质 LLEE 的进程图在互模拟坍缩下不封闭（不同于仅含真步转移且具 LLEE 的进程图）。我们通过为此类进程图定义保持 LLEE 的“结晶过程”绕开该障碍。由此我们得到具 LLEE 的“近坍缩”进程图，其强连通分量要么坍缩要么呈“双晶”形状。此类近坍缩进程图保证了正则表达式进程解释的互模拟坍缩具有可证解。
引用
@article{arxiv.2209.12188,
title = {Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete (Crystallization: Near-Collapsing Process Graph Interpretations of Regular Expressions)},
author = {Clemens Grabmayer},
journal= {arXiv preprint arXiv:2209.12188},
year = {2022}
}
备注
Version article submitted to LICS 2022 (with some corrections performed already during the review process, a few afterwards, 14 pages, 2 pages of the appendix)