可判定可逆等价性在有限Petri网中的研究：因果网双相似性与位置双相似性

《Information and Computation》：Decidable reversible equivalences for finite Petri nets

　　

在Petri网语境下，研究人员综述了真正并发谱系中的若干行为等价关系，以检验其中哪些是可逆的和可判定的。此处可逆意味着双相似的标识（marking）不仅能够匹配彼此的前向变迁，还能够通过撤销已发生的事件来匹配后向变迁。等价地，一个行为等价关系是可逆的，当且仅当它与它的遗传版本相一致。众所周知，被广泛研究的历史保持双相似性（history-preserving bisimilarity）不是可逆的，因为遗传历史保持（hereditary history-preserving, hhp）双相似性严格更精细。因此，研究人员寻找hhp双相似性的可逆、可判定、更精细的近似。作为主要贡献，研究人员展示并证明了两个这样的可逆等价关系，即因果网双相似性（causal-net bisimilarity）[Van Glabbeek, 2015]和位置双相似性（place bisimilarity）[Autant et al., 1991]。

研究背景方面，传统的行为等价关系关联的是具有等价未来行为的状态（或标识、或配置）。在确定性有限自动机（DFA）中，两个状态若识别相同语言则等价；在标记变迁系统（LTS）中，两个状态若沿箭头方向互相模拟彼此行为并导致双相似状态对，则为双模拟等价。当考虑需要撤销过去事件的系统时——例如乐观模拟中处理遗漏的依赖关系、工业机器人出错时重做动作、或可逆调试中通过回溯找出导致可见故障的缺陷——所关注的行为等价关系考虑后向变迁是有用的。研究人员将可逆行为等价关系称为这样一种行为等价关系：相关系统不仅能匹配其前向行为，还能匹配其过去行为，从而通过撤销某些已执行事件，所到达的状态仍然是等价的。De Nicola、Montanari和Vaandrager提出了来回双模拟（back and forth bisimulation），作为LTS上普通双模拟的增强，并证明这两种定义诱导出相同的等价关系。在LTS上，双模拟等价和分支双模拟等价都是自可逆的行为关系。为对并发系统建模，人们提出了真正并发模型，如事件结构、配置结构或Petri网。在配置结构中，过去历史不是从初始配置到当前配置执行事件序列σ所获得的实际计算路径，而是通过执行σ的任意与偏序兼容的排列所能到达的整个配置集合。这种可逆性概念被称为因果一致可逆性（causal-consistent reversibility）。本文的主要目的是综述真正并发谱系中的若干行为等价关系，以检验其中哪些是可逆的和可判定的，从最流行的历史保持双相似性（hp-bisimilarity）开始，其在Petri网上表现为完全并发双相似性（fc-bisimilarity）。hp-bisimilarity在事件结构上的来回版本被称为遗传历史保持双相似性（hhp-bisimilarity），它要求当两个系统通过回溯其历史来撤销动作时，hp-双模拟条件也成立。因此，hhp-bisimilarity是可逆等价关系，实际上是尊重因果性的最粗的可逆双模拟行为关系。然而，hp-bisimilarity不是自可逆的，因为hp-bisimilarity严格粗于hhp-bisimilarity。此外，虽然hp-bisimilarity在BPP网、安全有限Petri网和有界有限Petri网上是可判定的，但hhp-bisimilarity的可判定性结果要差得多；事实上，它在BPP网上可判定，但即使在安全网上也是不可判定的。因此，研究人员寻找有限Petri网上hhp-bisimilarity的可逆、可判定、更精细的近似。研究人员在文献中找到两个这样的等价关系，即因果网双相似性（记为～cn）和位置双相似性（记为～p）。因果网双相似性关联生成共享相同底层因果网（也称出现网）的网进程的标识。因此，因果网双相似的标识必须具有相同的大小，且匹配的变迁必须具有相同的形状。此外，因果网双相似性可以通过结构保持双相似性（structure-preserving bisimilarity，记为～sp）在Petri网上以简单方式刻画，后者在有界有限Petri网上是可判定的。位置双相似性比因果网双相似性更精细，但在整个有限（可能无界）Petri网类上是可判定的。本文的主要贡献可概括如下：定义了遗传因果网双模拟（hereditary causal-net bisimulation，定义14），通过用后向变迁扩展因果网双模拟的定义，其诱导的等价关系记为～hcn；证明了～cn和～hcn重合（定理1），这意味着因果网双相似性是自可逆的。类似地，通过用后向变迁扩展完全并发双模拟的定义，定义了遗传完全并发双模拟（定义16）；诱导的可逆行为关系记为～hfc，它是事件结构上定义的hhp-bisimilarity在Petri网上的移植；还证明了～cn比～hfc更精细（命题4）。直接证明了位置双相似性～p比因果网双相似性～cn更精细（定理2），而先前的结果利用了～cn作为～sp的刻画。证明了位置双相似性～p是自可逆的（定理3）。由于位置双相似性在有限Petri网上是可判定的，当标记Petri网无界时，它可作为因果网双相似性的替代方案。图1总结了本文综述的六种行为等价关系之间的关系，其中每个箭头都标注了证明该蕴含关系的定理或命题。图中还纳入了在事件结构上定义的灰色～hp和～hhp，因为它们分别是Petri网上～fc和～hfc的类似物。图中所示单一蕴含关系的逆均不成立。此外，～p是自可逆的（定理3）。本文组织如下：第2节回顾Petri网的基本定义；第3节定义Petri网的因果语义，包括因果网双模拟、完全并发双模拟，以及遗传因果网双模拟和遗传完全并发双模拟的新定义；该节还包含因果网双相似性与遗传因果网双相似性重合以及位置双相似性蕴含因果网双相似性的证明；第4节表明位置双相似性也是自可逆的；第5节讨论一个关于两个无界生产者-消费者系统的小型案例研究，展示该方法的适用性；最后，第6节概述相关文献并提示一些可能的未来研究方向。在结论部分，研究人员探讨了文献中先前未考虑的问题，即Petri网的真正并发双相似性是否是自可逆的，意味着它们能够通过回溯来匹配行为。作为主要结果，研究人员证明了因果网双相似性和位置双相似性都是自可逆的。后者特别有趣，因为位置双相似性在有限（但可能无界）Petri网上是可判定的，这使研究人员能够用它来证明给定规范的非平凡实现的正确性。这两种行为关系是hhp-双相似性的更精细的可判定可逆近似。关于hhp-双相似性的更粗可判定近似，Fr?schle和Hildebrandt提出了一个无限层次的雙相似性概念，所有这些在安全有限Petri网上都是可判定的，它们精化（他们自己的变体定义的）hp-双相似性，且比hhp-双相似性更粗，使得hhp-双相似性是层次中所有雙相似性的交集。然而，这一结果对本文目的不太有用，因为hhp-双相似性的更粗近似不能确保可逆性。一个显而易见的问题是因果网双相似性是否是充分尊重因果性的最粗自可逆行为关系。答案是否定的。事实上，通过改编定理1的证明可以证明，更粗的i-因果网双相似性～icn也是自可逆的。该等价关系确保相关标识生成相同的因果网，位于因果网双相似性和hfc-双相似性之间；事实上，图6中的标识是i-因果网双相似的（但不是因果网双相似的），而图5中的两个网是遗传完全并发双相似的（但不是i-因果网双相似的）。i-因果网双相似性在有界Petri网上是可判定的；该证明基于在有序索引标识上的一种相当复杂的等价双模拟刻画，这解释了为什么研究人员选择直接处理因果网双相似性，后者通过结构保持双相似性以简单方式刻画。由于文献中没有其他位于～icn和～hfc之间的等价关系，i-因果网双相似性似乎是Petri网上可定义的最粗自可逆尊重因果性的基于双模拟的行为关系的自然候选者。表1总结了本文讨论的前向唯双模拟行为关系的技术性质。位置双相似性～p是唯一享有所有性质的关系。另一个自然问题是：给定三个等价关系E、E1和E2，如果（i）E是自可逆的，（ii）E1比E精细，且（iii）E2是E1的遗传强化，那么E1和E2是否重合？答案是否定的：只需考虑E=～int、E1=～fc和E2=～hfc。然而，如果E也是尊重因果性的，那么研究人员猜想E1=E2。研究人员所解决的问题不同于[46,47]或[20,48]中的问题，后者的焦点分别是理解向Petri网添加单个变迁的逆的影响，或添加每个变迁的逆以便能够在历史上回溯。相反，研究人员不向Petri网添加逆变迁，而是定义一个可逆行为等价关系，确保行为等价的标识不仅能匹配其前向行为，还能通过撤销事件来匹配其后向行为。研究人员猜想，如果两个网根据可逆行为等价关系是等价的，那么它们如[20]中定义的扩展也是等价的。未来工作的另一个方向是将结果应用于CCS。事实上，CCS和其他进程代数已被赋予Petri网语义。研究人员之一在[15]中表明，CCS的一个方言Pet足以表示所有且仅表示有限P/T网，直至同构。因此，得益于本文证明的结果，研究人员得出结论：位置双相似的Pet进程项能够以因果一致的方式匹配其前向和后向行为。此外，位置双相似性是Pet代数算子上的同余，因此可以以进程代数界惯用的风格组合地验证实现与其规范的等价性。