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

郝宗寅 等:Petri 网的反向展开及其在程序数据竞争检测的应用 1629

定理 1. ≺ r 是 adequate order.
证明:易得≺ r 满足 adequate order 的条件(1)、条件(2).只需证明≺ r 满足条件(3)即可.即证明:当 Mark(Cfg 1 )≤
Mark(Cfg 2 )∧Cfg 1 ≺ r Cfg 2 时,对 Cfg 2 的任意前缀 E 2 ,有 E 1 满足 Mark(Cfg 1 ⊕E 1 )≤Mark(Cfg 2 ⊕E 2 ),且 Cfg 1 ⊕E 1 ≺ r Cfg 2 ⊕
E 2 .
k
k
定义 Ek 为配置 Cfg 的一个大小为 k 前缀,Cfg =Cfg⊕E .接下来按|E 2 |的大小进行归纳证明.|E 2 |=0 时,结论显
k
k
然成立.|E 2 |=k 时,由归纳假设有 Mark (Cfg 1 k )≤ Mark (Cfg k 2 ) ,且 Cfg ≺ r Cfg .|E 2 |=k+1 时,对任意变迁 t.
2
1
i
• 设 e 2 =(t,C 2 ), (Cμ 2 ) ⊆ t ∧ C ⊆ 2 Cut (Cfg 2 k ) ,有 Cfg k + 1 = Cfg ∪ 2 k {}e ;
2
2
i
• 设 e 1 =(t,C 1 ), ()Cμ 1 ⊆ t ∧ C ⊆ 1 Cut (Cfg 1 k ) ,有 Cfg 1 k + 1 = Cfg ∪ 1 k {}e .要求μ(C 1 )≤μ(C 2 )且 C 1 尽可能大(C 1 可
1
以为∅).
接下来只需证明 Mark (Cfg 1 k + 1 )≤ Mark (Cfg 2 k + 1 ) ,且 Cfg 1 k + 1 ≺ r Cfg 2 k + 1 ,有以下两种情况.
k
(1) C 1 =∅: Cfg = Cfg 1 k + 1 .由于要求了 C 1 尽可能大,可知:∀p∈μ(C 2 ), p∉ Mark (Cfg 1 k ) ,易得 Mark (Cfg 1 k + 1 ) =
1
Mark (Cfg 1 k )≤ Mark (Cfg 2 k ) μ− (C + 2 ) i t = Mark (Cfg 2 k + 1 ) . 又因为 | Cfg 2 k | | Cfg< 2 k + 1 | , 由 ≺ r 的定义 (1), 有
k
Cfg ≺ Cfg k + 1 ,进而有 Cfg k + 1 = Cfg ≺ k Cfg ≺ k Cfg k + 1 .C 1 =∅时结论成立;
2 2 1 1 r 2 r 2
(2) C 1 ≠∅:由于要求了 C 1 尽可能大,且μ(C 1 )≤μ(C 2 ),可知:∀p∈μ(C 2 ), p μ∈ ()C ∨ 1 p∉ Mark (Cfg 1 k ) ,易得
Mark (Cfg 1 k + 1 ) = Mark (Cfg 1 k ) μ − ( )C + 1 i t ≤ Mark (Cfg 2 k ) μ − (C + 2 ) i t = Mark (Cfg 2 k + 1 ) . 当 | Cfg 1 k | | Cfg< k 2 | 时 ,
有 | Cfg k + 1 | | Cfg= k | 1 | Cfg+ < k | 1 | Cfg+ = k + 1 |,Cfg k + 1 Cfg≺ k + 1 . 当 | Cfg k | | Cfg= k | , 且 Lex ((Cfgμ k )) <
1 1 2 2 1 r 2 1 2 1
Lex ((Cfgμ k 2 )) 时,有 | Cfg 1 k + 1 | | Cfg= 1 k | 1 | Cfg+ < k 2 | 1 | Cfg+ = 2 k + 1 | .两个长度相同的有序串添加一个相同元素
并重新排序后,二者间的字典序大小关系不会发生改变,因此 Lex ( (Cfgμ 1 k + 1 )) < Lex ( (Cfgμ k + 2 1 )),Cfg 1 k + 1 ≺
r
Cfg k + 1 .C 1 ≠∅时结论成立.
2
综上,有 Mark(Cfg 1 ⊕E 1 )≤Mark(Cfg 2 ⊕E 2 ),且 Cfg 1 ⊕E 1 ≺ r Cfg 2 ⊕E 2 .因此,≺ r 是 adequate order. □
定理 2. 反向截断事件不会破坏 RUnf 的完备性.
证明:对于满足 M M f 的任意可达标识 M,应存在配置 Cfg 满足 Mark(Cfg)⊆M.假设 Cfg 不存在于 RUnf 中,
则 Cfg 中一定包含反向截断事件 e,且 RUnf 中存在事件 e′,使得 Mark([e′])≤Mark([e])∧[e′]≺[e].
由 adequate order 的条件(3)可知:对于 Cfg=[e]⊕E,存在 Cfg′=[e′]⊕E′,使得 Mark(Cfg′)≤Mark(Cfg)≤M∧Cfg′≺
Cfg.由于≺是良基的,上述过程最终会找到一个存在于 RUnf 中的极小配置,这与假设不符.故反向截断事件不会
破坏 RUnf 的完备性. □
定理 3. RUnf 是有限的.
证明:对于 RUnf 内的任意事件 e,可以得到一条最长链 e 1 <e 2 <…<e,设其长度为 d(e),有以下 3 个结论.
•
•
•
•
(1) 对于任意条件 c, c 与 c 是有限的;对于任意事件 e, e 与 e 是有限的;
(2) 设安全 Petri 网的可达标识总数为 n,有 d(e)≤n+1.长度为 n+1 的链 e 1 <e 2 <…<e n+1 必然存在两个事件
e i ,e j ,i<j,使得 Mark([e i ])≤Mark([e j ]).又因为[e i ]⊂[e j ],由 adequate order 的条件(2)可知[e i ]≺[e j ],e j 为反向
截断事件.由此可知,链中不存在 e 使得 e j <e,即链长不可能大于 n+1;
(3) 对于任意 k(k≥0),RUnf 中仅包含有限多的事件 e,使得 d(e)≤k.
可以进行归纳证明:k=0 时,结论显然成立.设 E k 为 d(e)≤k 的事件集合,由归纳假设可知,E k 是有限的.E k+1 为
•
•
d(e)≤k+1 的事件集合.由 E k+1 ⊆ E k ∪CM f 以及结论(1)可知,E k+1 是有限的.
由结论(2)、结论(3)可知,RUnf 包含有限多的事件;再由结论(1)可知,RUnf 包含有限多的条件,故 RUnf 是有
限的. □
附录 B

首先回顾一下 RExt 的两个条件.