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.

翻译：关于Milner（1984）提出的正则表达式模互模拟的进程语义的公理化与可表达性问题，对于包含死锁0和空步1的完整表达式类而言已被证明具有难度。我们报告了当存在0时引入1所产生的一种现象，该现象聚焦了造成此困难的关键原因。具体而言：虽然无1正则表达式的解释在互模拟坍塌下封闭，但任意正则表达式的解释并不如此。无1正则表达式的进程图解释满足循环存在与消除性质LEE，且该性质在互模拟坍塌下保持。LEE的这些特征曾被用于证明：无1正则表达式模互模拟的等式证明系统是完备的，并且判定进程图是否与无1正则表达式解释互模拟可以在多项式时间内完成。尽管正则表达式的解释通常不满足LEE性质，但我们通过精炼解释（即带有1-转移的图，类似于自动机中的静默步）可恢复LEE。这表明LEE对于一般的公理化与可表达性问题也可能是有用的。但出现了一个需要解决的新现象：进程图“可被精炼为带有1-转移且满足LEE的进程图”的性质在互模拟坍塌下不保持。我们构造了一个具有两个1-转移的10顶点图，该图满足LEE，但其中一对互模拟顶点在保持精炼性质的前提下无法相互坍塌。这意味着正则表达式进程解释的像在互模拟坍塌下不封闭。