Page 56 - 《软件学报》2021年第6期

1630 Journal of Software 软件学报 Vol.32, No.6, June 2021

•
(1) 对于 RUnf 中任意事件 e,RExt 中不存在反向扩展 rext=(t,C),使得μ(e)=t∧e =C;
(2) 对于 RExt 内 任意两不同 的反向扩展 rext 1 =(t 1 ,C 1 ),rext 2 =(t 2 ,C 2 ), 若 t 1 =t 2 ∧C 1 ⊂C 2 ∧Mark([rext 1 ])≥
Mark([rext 2 ]),则将扩展 rext 1 从 RExt 中删除.
Parosh 在文献[19]中首次提出了反向展开的思想,但未在扩展规则中加入 Mark([rext 1 ])≥Mark([rext 2 ])这个
限制,由此导致其反向展开不满足完备性.这里分析其反例.
考虑图 11 所示的 Petri 网及其反向展开.左图是原 Petri 网,目标标识为{p12},不难发现,目标标识是可覆盖
的.右图是未加限制条件 Mark([rext 1 ])≥Mark([rext 2 ])时的反向展开.反向展开算法在生成事件 e8 时对应的反向
扩展为 rext1=(t8,{c2,c9}),根据 Parosh 的规则会丢弃 rext2=(t8,{c2}).然而,分析原 Petri 网会发现:rext1 对应的反
向标识{p4,p8}是不可覆盖的,而 rext2 对应的反向标识{p8,p11}是可覆盖的.进一步,rext2 对应的反向标识对判
断{p12}的可覆盖性来说是必要的,此时无论后续如何扩展都无法验证目标标识的可覆盖性,RUnf 的完备性已
被破坏.

Fig.11 Example on completeness destruction of reverse unfolding
图 11 反向展开完备性被破坏的实例

郝宗寅(1998－),男,硕士生,CCF 学生会 鲁法明(1981－),男,博士,副教授,博士生
员,主要研究领域为 Petri 网理论与应用, 导师,CCF 专业会员,主要研究领域为 Petri
并行程序形式化验证. 网理论与应用,并发系统建模与分析,业务
过程管理与决策支持.