论文标题
米尔纳（Milner）正式表达式的证明系统模型二比度已完成（结晶：近乎填充的过程图表的正则表达式解释）
Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete (Crystallization: Near-Collapsing Process Graph Interpretations of Regular Expressions)
论文作者
论文摘要
米尔纳（Milner，1984）为正则表达式定义了过程语义。他为正则表达式的过程解释制定了一个合理的证明系统，并询问该系统是否完成。 我们从概念上报告了一个证明，该证明表明米尔纳的系统是通过激励，说明和描述其所有主要步骤完成的。我们通过GrabMayer和Fokkink（2020）的完整性证明，以限制Milner系统“免费”正则表达式。作为一个关键并发症，我们认识到满足层状环的存在/消除属性llee的过程图未在双仿真崩溃下闭合（与仅具有适当步骤过渡的llee的过程图不同）。我们通过为此类过程图定义了保留LLEE的“结晶过程”来绕过这一障碍。这样，我们获得了用llee获得的“近乎收集”的过程图，其紧密连接的组件要么折叠或“双结晶”形状。这种近乎汇总的过程图保证了可仿真的溶解解决方案，以折叠正态表达式的过程解释。
Milner (1984) defined a process semantics for regular expressions. He formulated a sound proof system for bisimilarity of process interpretations of regular expressions, and asked whether this system is complete. We report conceptually on a proof that shows that Milner's system is complete, by motivating, illustrating, and describing all of its main steps. We substantially refine the completeness proof by Grabmayer and Fokkink (2020) for the restriction of Milner's system to `1-free' regular expressions. As a crucial complication we recognize that process graphs with empty-step transitions that satisfy the layered loop-existence/elimination property LLEE are not closed under bisimulation collapse (unlike process graphs with LLEE that only have proper-step transitions). We circumnavigate this obstacle by defining a LLEE-preserving `crystallization procedure' for such process graphs. By that we obtain `near-collapsed' process graphs with LLEE whose strongly connected components are either collapsed or of `twin-crystal' shape. Such near-collapsed process graphs guarantee provable solutions for bisimulation collapses of process interpretations of regular expressions.
