论文标题
1个免费正则表达式的完整证明系统Modulo Bisimarlity
A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity
论文作者
论文摘要
罗宾·米尔纳（Robin Milner，1984）给出了一个良好的证明系统，以解释为流程的正态表达式的双性恋系统：基本过程代数，带有Unary Kleene Star迭代，僵局0，成功的终止终止1和固定点规则。他问这个系统是否完成。尽管在过去的35年中进行了深入的研究，但问题仍然开放。 本文对米尔纳的问题给出了部分积极的答案。我们证明，米尔纳系统通过删除常数1的正则表达式的子类的适应，并通过更改为二进制kleene star迭代完成。我们使用的关键工具是图形结构属性，该属性可以通过正则表达式保证过程图的表达性，并且可以通过从过程图到其双仿真崩溃来保存。
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. This paper gives a partial positive answer to Milner's problem. We prove that the adaptation of Milner's system over the subclass of regular expressions that arises by dropping the constant 1, and by changing to binary Kleene star iteration is complete. The crucial tool we use is a graph structure property that guarantees expressibility of a process graph by a regular expression, and is preserved by going over from a process graph to its bisimulation collapse.
