无限制算子下的互模拟研究

我们重新审视无限制(restriction)算子的进程模型中的标准互模拟等式。众所周知，一般而言弱互模拟比强互模拟更粗，因为它从内部动作中抽象出来。在无限制的情况下，这些内部动作变得某种可见，因此人们可能想知道弱互模拟是否仍然是“弱”的。我们证明，在CCScore（即Milner的标准CCS，无$\tau$-前缀、求和与重标号）及其高阶变体（名为HOCCScore）中，弱互模拟确实保持弱，即仍严格粗于强互模拟，即便没有限制算子。这些结果可推广到其他一阶或高阶进程模型。本质上，这是由于复制操作的直接或间接存在，可使进程保持其状态（即交互能力）。借助这些观察，我们考察了一种弱互模拟的变体，称为准强互模拟。该准强互模拟要求内部动作的匹配以强方式进行，如同强互模拟，而可见动作的匹配不带尾随内部动作。我们展示在无限制算子的CCScore中，弱互模拟恰好坍缩到该准强互模拟上，且后者被证明与分支互模拟重合。这些结果表明，在缺少限制操作的情况下，弱互模拟的某些成分确实变为强，特别是内部动作的匹配。