论文标题
正则表达式过程语义的结构受限的过程图
Structure-Constrained Process Graphs for the Process Semantics of Regular Expressions
论文作者
论文摘要
米尔纳（Milner，1984）引入了一种用于过程图的正则表达式的过程语义。与语言语义不同的是，每个常规语言（即DFA）语言都是对某些正则表达式的解释，存在有限的过程图，这些图与任何正则表达式的过程解释都不是偶然的。对于通过正则表达式表达的图表的推理，希望在解释图像中具有过程图的结构表示。 对于“ 1 free”正则表达式，它们的过程解释满足结构性lee（循环存在和消除）。但这并不是所有正则表达式的情况，正如我们通过示例所示。然而，作为一种补救措施，我们描述了为过程解释的紧密变体回收财产的可能性。为此，我们完善了正则表达式的过程语义，以产生1个过渡的过程图，类似于有限状态自动机的无声移动。 该报告伴随着论文在2020年讲习班期间的邮政审进后带有相同的标题。在这里，我们不仅给出了两个中央定理中的两个证明。
Milner (1984) introduced a process semantics for regular expressions as process graphs. Unlike for the language semantics, where every regular (that is, DFA-accepted) language is the interpretation of some regular expression, there are finite process graphs that are not bisimilar to the process interpretation of any regular expression. For reasoning about graphs that are expressible by regular expressions modulo bisimilarity it is desirable to have structural representations of process graphs in the image of the interpretation. For `1-free' regular expressions, their process interpretations satisfy the structural property LEE (loop existence and elimination). But this is not in general the case for all regular expressions, as we show by examples. Yet as a remedy, we describe the possibility to recover the property LEE for a close variant of the process interpretation. For this purpose we refine the process semantics of regular expressions to yield process graphs with 1-transitions, similar to silent moves for finite-state automata. This report accompanies the paper with the same title in the post-proceedings of the workshop TERMGRAPH 2020. Here we give the proofs of not only one but of both of the two central theorems.
