Axiomatization and expressibility problems for Milner's process semantics (1984) of regular expressions modulo bisimilarity have turned out to be difficult for the full class of expressions with deadlock 0 and empty step~1. We report on a phenomenon that arises from the added presence of 1 when 0 is available, and that brings a crucial reason for this difficulty into focus. To wit, while interpretations of 1-free regular expressions are closed under bisimulation collapse, this is not the case for the interpretations of arbitrary regular expressions. Process graph interpretations of 1-free regular expressions satisfy the loop existence and elimination property LEE, which is preserved under bisimulation collapse. These features of LEE were applied for showing that an equational proof system for 1-free regular expressions modulo bisimilarity is complete, and that it is decidable in polynomial time whether a process graph is bisimilar to the interpretation of a 1-free regular expression. While interpretations of regular expressions do not satisfy the property LEE in general, we show that LEE can be recovered by refined interpretations as graphs with 1-transitions refined interpretations with 1-transitions (which are similar to silent steps for automata). This suggests that LEE can be expedient also for the general axiomatization and expressibility problems. But a new phenomenon emerges that needs to be addressed: the property of a process graph `to can be refined into a process graph with 1-transitions and with LEE' is not preserved under bisimulation collapse. We provide a 10-vertex graph with two 1-transitions that satisfies LEE, and in which a pair of bisimilar vertices cannot be collapsed on to each other while preserving the refinement property. This implies that the image of the process interpretation of regular expressions is not closed under bisimulation collapse.

翻译：关于米尔纳(1984)提出的正则表达式互模拟过程语义的公理化和可表达性问题，对于包含死锁0和空步1的完整表达式类而言已被证明十分困难。我们报告了当0存在时引入1所产生的新现象，这揭示了该困难的关键原因：尽管无1正则表达式的解释在互模拟坍缩下封闭，但任意正则表达式的解释却不满足这一性质。无1正则表达式的过程图解释满足循环存在与消除性质LEE，该性质在互模拟坍缩下保持不变。LEE的这些特征曾被用于证明：无1正则表达式在互模拟意义下的等式证明系统是完备的，且判定过程图是否双模拟于无1正则表达式解释的问题可在多项式时间内解决。虽然正则表达式的解释一般不满足LEE性质，但我们证明可通过精化解释为带1转移的图（类似于自动机中的静默步）来恢复LEE。这表明LEE对于一般的公理化和可表达性问题同样有效。然而需要解决一个新现象：过程图"可被精化为带1转移且满足LEE的图"这一性质在互模拟坍缩下不保持。我们构造了一个含10个顶点和两条1转移的图，该图满足LEE，但其中一对互模拟顶点在保持精化性质的条件下无法互相坍缩。这意味着正则表达式过程语义解释的像在互模拟坍缩下不封闭。