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

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

进行剪枝、亦或是使用启发式技术优化算法效率,但在正向分支过多的情况下,还是难以避免对系统冗余行为
的分析.同样,即使反向展开配备了启发式技术,在反向分支过多时,也难以保证算法的效率.在这个前提下,本节
进而通过实例表明,反向展开在某些情况下优于正向展开.接下来将详细介绍反向展开算法.

2 Petri 网的反向展开

2.1 反向展开的概念
2.1.1 Petri 网
一个网可以定义为一个三元组(P,T,F),P 为库所集,T 为变迁集,F 为 P 与 T 间的流关系,F⊂(P×T)∪(T×P).节
•
•
点 x 的前集定义为 x={y∈P∪T|F(y,x)=1},节点 x 的后集定义为 x ={y∈P∪T|F(x,y)=1}.网(P,T,F)的标识是建立在 P
上的一个多重集.在图形化表示时,网的标识通过在各个库所中添加相应数量的 token 来表示.
一个网系统可以定义为一个四元组(P,T,F,M 0 ),其中,M 0 是网(P,T,F)的初始标识.如果∀p∈P:F(p,t)≤M(p),则
标识 M 下变迁 t 使能,使能的变迁可以执行.t 的执行使系统进入一个新的标识 M′,记作 M ⎯⎯→ M ′ ,即:对每个库
t
所 p,M′(p)=M(p)−F(p,t)+F(t,p).一个变迁序列σ=t 1 t 2 …t n 称之为触发序列,当且仅当存在标识 M 1 ,M 2 ,…,M n−1 ,M n ,
σ
使得 M ⎯⎯→ 0 1 t M ⎯ 1 ⎯ 2 t →⎯⎯⎯→ n t 1 − M n− 1 ⎯ ⎯ n t → M 成立.上式也可以表示为 M ⎯⎯→ M ,称 M n 是触发序列σ下的可
...
0
n
n
达标识.
对于标识 M f ,若有标识 M,M′和触发序列σ,使得 M ⎯⎯→ σ M ′ ∧ M ⊆ f M ′ ,则称 M f 可被 M 覆盖,记为 M M f .
若可达标识 M 满足∀p:M(p)≤n,则称 M 是 n-safe 的.一个网系统是 n-safe 的,当且仅当其所有可达标识都是
n-safe 的.特别地,将 1-safe 网系统称为安全网系统.本文只考虑安全 Petri 网的可覆盖性问题,并记可覆盖性判定
的目标标识为 M f ,即验证 M 0 M f 是否成立.
2.1.2 反向出现网
定义 1(反向出现网). 反向出现网是出现网的子类,用以判定一个 Petri 网中目标标识 M f 的可覆盖性,对应
一个四元组 RON=(C,E,F′,CM f ).其中,C 为条件集,每个条件对应 Petri 网库所中的一个 token;E 为事件集,每个事
件对应 Petri 网中某变迁的一次执行;F′为 C 与 E 间的流关系,对应 Petri 网的流关系;CM f 为 Petri 网目标标识
•
M f 在 RON 中对应的条件集合,满足∀c∈CM f :c =∅.
以图 3(a)中的 Petri 网与目标标识 M f ={p4}为例,它对应的反向出现网见图 3(b),其中,CM f ={c1}.

(a) Petri 网实例 (b) 反向出现网实例
Fig.3 An example of Petri net and its reverse occurrent net
图 3 Petri 网实例及其对应的反向出现网

RON 上的两个节点 x 1 ,x 2 有以下 3 种关系.
(1) 反向因果:若从 x 1 出发的某条路径可到达 x 2 ,则记 x 2 ≤x 1 .特别的,对于任意节点 x,有 x=x.图 3(b)中,有
c1≤c5,e2≤e3;
•
•
(2) 反向冲突:若存在两个不同的事件 e 1 ,e 2 ∈E,e 1 ∩e 2 ≠∅∧e 1 ≤x 1 ∧e 2 ≤x 2 ,则称 x 1 与 x 2 反向冲突,记为 x 1 #x 2 .
•
•
图 3(b)中,c2 与 c3 反向冲突,这是因为 e1≤c2,e2≤c3,且 e1 ∩e2 ={c1}≠∅.同理,c2 与 c4 反向冲突、e1