基于部分状态空间存储的Petri网库所界求解算法

卢委红，丁志军

1.同济大学电子与信息工程学院，上海201804

2.同济大学教育部嵌入式系统与服务计算重点实验室，上海201804

3.同济大学上海市电子交易与信息服务协同创新中心，上海201804

Petri 网是一种重要的形式化建模工具，能有效地对信息系统进行描述和建模.作为一种系统模型，Petri 网不仅可以刻画系统的结构，还可以描述系统的动态行为；既有直观的图形表示，又可以引入许多数学方法分析其性质.Petri 网具有可达性、有界性、活性等[1]重要的性质，同Petri 网所模拟的实际系统联系密切.

在这些性质中，Petri 网的有界性[2]反映了被模拟系统运行过程中对有关资源的容量要求.如果能够求出每个库所p的界b，那么在系统设计时，只要库所p所表示资源的容量不小于b，就能保证系统正常运行.此外，库所界的信息还可以指导可达标识的存储，通过位存储的方式减少存储可达标识所需的空间.也就是说，若已知库所p的界为b，则只需lbb比特的存储空间来存储该库所的标识数.

目前求解库所界的方法有两种：一种方法是完全生成状态空间[2-3]，但对存储空间的要求过高；另一种方法是用P 不变量估计库所界[4]，但存在无法精确求解所有库所界的问题.为此，本文提出了一种基于部分状态空间存储求解库所界的算法，在Petri 网生成状态空间的过程中，只需存储其中一部分能标识就可以精确求解所有库所的界.实验中选取了模型检测竞赛中的部分模型，并对3 种求解界的方法进行了比较分析，实验结果说明了本文算法的有效性.

1 相关工作

Petri 网中库所界的含义是系统运行过程中库所p获得标识数的最大值.库所界的概念提出后，Finkel[3]提出了求解库所界的方法，即从Petri 网的初始标识开始运行整个Petri 网系统，在此过程中记录全部库所的最大托肯值，从而精确求解Petri 网中全部库所的界.然而，该方法需要生成、记录并存储所有可达标识，对系统存储空间要求较高.

2019年，Wolf[4]提出用P 不变量方法估计库所界，以压缩每个标识所需的存储空间.若i是1 个P 不变量，则对于所有可达标识m有m(p)≤，从而求解得到库所p的估计界.该方法存在如下问题：1）P 不变量无法覆盖全部库所；2）即使是大于零的分量所对应的库所，仍然存在界估计不准确的问题.例如，图1(a)所示的Petri 网PN0中P 不变量为(2,1,1,1,1).由P 不变量的性质可得，在任何可达标识m下，满足2m(p1)+m(p2)+m(p3)+m(p4)+m(p5)=2，则库所p2的上界估计为2.而通过生成可达图可以得到该库所的上界实际为1，如图1(b)所示，因此实际只需1 比特来存储.

图1 Petri 网PN0 及其可达图Figure 1 Petri net PN0 and its reachability graph

Schmidt[5-6]提出在生成Petri 网状态空间时，用T不变量方法只存储部分状态空间来验证Petri 网的可达性、死锁等性质.该方法通过求解T不变量存储可达图中的部分标识，以保证可达图生成的正常终止，减少了验证Petri 网性质过程中所需的存储空间.同时该方法在验证相关性质的过程中会访问到每一个状态，保证了验证结果的正确性.但该方法没有讨论Petri 网的有界性及库所界的求解.

本文提出了一种基于部分状态空间存储求解库所界的算法，在Petri 网生成状态空间的过程中，只需存储其中一部分状态就能精确求解所有库所的界.与完全生成状态空间的方法[3]相比，本文算法由于只存储部分标识，减少了所需的空间资源.与P 不变量估计库所界方法[4]相比，本文算法可以精确求解所有库所的界，提高了库所界求解的精确度.

2 基本概念

Petri 网是用于描述分布式系统的一种模型，既能够描述系统的结构，又能够模拟系统的运行.利用Petri 网为一个实际系统建模时，网的部分描述系统的结构，可以将每个库所看作一个条件，每个变迁看作一个事件，事件有发生权当且仅当它的每个前置条件都成立.标识部分反映系统的状态，包含事件发生前后的状态.

假设N是自然数的集合，Petri 网的一些基本概念[7]如下：

定义1（Petri 网）

Petri 网是一个五元组PN=(P,T,F,W,M0)，其中P和T是两个不相交的有限集合，P中元素称为库所，T中元素称为变迁.F是有向弧的集合，定义为F ⊆(P ×T)∪(T ×P).W是弧的权重函数，定义为W:F→N.当(x,y)/∈F时，W(x,y)=0.M0是初始标识.网PN 的一个标识M是一个映射M:P→N，表示标识M下各个库所的托肯分布，其中M(p)表示标识‘M下库所p中的托肯数目.

定义2

给定一个Petri 网PN，x•={y|(x,y)∈F}，•x={y|(y,x)∈F}，其中x,y ∈P ∪T.若x是库所（变迁），则•x称为x的输入变迁（库所）集合，x•称为x的输出变迁（库所）集合.

定义3（变迁发生规则）

给定一个Petri 网PN，在一个标识M下，对于一个变迁t ∈T，若∀p ∈•t，M(p) ≥W(p,t)，则称变迁t在标识M下使能，使能变迁可以发生并产生新标识M＇，记为M[t>M＇，满足∀p ∈P，M＇(p)=M(p)−W(p,t)+W(t,p).

定义4（可达性）

给定一个Petri 网PN，若存在t ∈T，使得M[t>M＇，则称M＇为从M直接可达的.若存在变迁序列t1,t2,···,tk和标识序列M1,M2,···,Mk使得

则称Mk为从M可达的.从M可达的一切标识的集合记为R(M).

定义5（可达图）

给定一个Petri 网PN，PN 的可达图定义为一个三元组RG(PN)=(R(M0),E,P)，其中

称R(M0)为RG(PN)的顶点集，E为RG(PN)的弧集；若P(Mi,Mj)=tk，则称tk为弧(Mi,Mj)的旁标.

例如，图2是一个Petri 网模型，库所用圆圈表示，变迁用矩形表示，弧用有向边表示.若边上没有标记，则默认弧的权重为1.初始托肯用库所中的黑点表示.

图2 Petri 网模型——ERKFigure 2 Petri net model—ERK

定义6（有界性）

给定一个Petri 网PN，p ∈P.若存在正整数B，使得∀M ∈R(M0):M(p)≤B，则称库所p为有界的，并称满足此条件的最小正整数B为库所p的界，记为B(p)，即B(p)=min{B|∀M ∈R(M0):M(p)B}.当B(p)=1 时，称库所p是安全的.

定义7（关联矩阵）

给定一个Petri 网PN，P={p1,p2,···,pm}，T={t1,t2,···,tn}，则Petri 网PN 的结构可以用一个m行n列矩阵A=[aij]m×n表示，其中aij=W(tj,pi)−W(pi,tj),i ∈{1,2,···,m}，j ∈{1,2,···,n}，称A为网PN 的关联矩阵.

定义8（状态方程）

给定一个Petri 网PN，A为网PN 的关联矩阵.若M ∈R(M0)，则存在非负整数的n维向量X，使得

则该式称为Petri 网的状态方程.式(3)中的n维非负整数向量X称为发生数向量.如果M是从M0可达的，则使得M0[σ >M的任意一个变迁序列σ都有一个满足状态方程的n维向量X，使得#(ti/σ)=X(i)，即X中的第i个分量等于ti在σ中出现的次数.

定义9（P 不变量）

给定一个Petri 网PN，|P|=m，|T|=n，A为PN 的关联矩阵.若存在非平凡的m维非负整数向量X满足ATX=0，则称X为网PN 的一个P 不变量.

结合状态方程可得，若标识从标识m可达，则满足=Xm.若p是一个库所，满足X(p)0，可得

例如，在图2所示的Petri 网中，(1,0,1,1,0,0,0,0,0,0,0)T为一个P 不变量.

定义10（T 不变量）

给定一个Petri 网PN，|P|=m，|T|=n，A为PN 的关联矩阵.若存在非平凡的n维非负整数向量Y满足AY=0，则称Y为网PN 的一个T不变量.

从一个标识m下发生T 不变量Y中非零分量的变迁，能再次产生标识m，反映了可达图中状态的回路关系.

例如，在图2所示的Petri 网中，初始标识下可以发生变迁序列t1,t2,并再次产生初始标识.因此(1,1,0,0,0,0,0,0,0,0,0)T为一个T 不变量.

3 基于部分状态空间的Petri 网库所界求解算法

3.1 算法原理

如前所述，本文算法的主要思想为，在不存储Petri 网的所有状态，实现所有库所精确界的求解.该算法核心在于所存储的部分状态既能保证从这些状态出发可以遍历到Petri网的所有可达状态，以准确获取每个库所中的托肯数进而计算库所界；又能确保可达图生成算法的终止.这其中，由于Petri 网的可达状态都可由初始状态依据Petri 网变迁发生规则计算产生，所以理论上只要保存包含初始状态的部分状态一定是可以遍历到Petri 网的所有可达状态.因此算法需主要解决第二个问题，即只存储部分状态如何保证可达图生成算法的正常终止.

进一步分析可知，该情况下可达图生成算法无法终止的原因是在可达图中有回路的存在.所谓回路，即从一个状态出发，发生一个变迁序列后能再次产生该状态.显然对于可达图中的某个状态m：

1）若状态m在一个回路内，假设该回路中任何一个状态都没有存储和记录，则在可达图生成过程中由于无法判断状态m之前是否生成过，所以会不断重复生成该状态，导致可达图会一直生成.

2）若状态m不存在于任何一个回路内，即状态m在可达图生成过程中只会产生一次，则无需存储状态m也能够保证可达图的终止.特别地，若可达图中没有回路，则只需记录初始状态就能保证可达图生成算法的终止.

通过上述分析可知，对于状态m所在的回路至少需要存储回路上的一个状态才能保证算法不会陷入无限循环，确保算法终止.

下面利用Schmidt[5]的方法，通过T不变量的性质找到覆盖可达图中所有回路的状态集合，通过存储这些状态可以保证可达图中的每个回路都至少存储了一个状态，从而实现可达图生成算法的正常终止.

对关联矩阵A进行初等行变换能够将其转化成上三角形式[4]，即某行最左边的非零元素总在之前行最左边非零元素的右边.将包含某行最左边非零元素的列称为头列，其余列称为尾列.

如图3所示，矩阵A为图2中Petri 网关联矩阵的上三角形式，t1,t3,t5,t6,t8,t9所在的列为头列，t2,t4,t7,t10,t11所在的列为尾列.

图3 关联矩阵的上三角形式AFigure 3 Upper triangular form A of incidence matrix

矩阵A的每一列对应变量x，因此可以将变量分为头变量和尾变量.在本例中头变量为x1,x3,x5,x6,x8,x9，尾变量为x2,x4,x7,x10,x11.

定义11（Uset）

将关联矩阵转化为上三角形式后，所有尾变量对应的变迁集合称为Uset.在本例中，Uset={t2,t4,t7,t10,t11}.

实际上，变迁集合Uset是覆盖所有T 不变量的最小变迁集合.因为集合Uset中的元素为与所有尾变量对应的变迁集合，而对所有尾变量赋值为1、所有头变量赋值为0 的向量I表示所有T 不变量的线性组合，并且是覆盖变迁数目最少的一个线性组合.因此向量I中非零元素组成的集合Uset是覆盖所有T 不变量的最小变迁集合.只要存储发生Uset中的变迁产生的标识集合就意味着可达图中的每个回路都至少存储了一个状态.

通过前述分析可知，可达图中每个回路都需要存储一个状态以保证生成算法的终止.如果能够消除可达图中的回路，就有可能进一步减少求取界过程中需要存储的状态数目.为此，本文引入了变迁对、变迁环的概念，通过识别变迁对、变迁环，抑制部分变迁的发生，在不影响状态生成的同时，避免可达图回路的产生.

3.1.1 变迁对

定义12（支集、变迁对）

设X为网PN 的一个T 不变量，记

称为T 不变量X的支集.特别地，若满足X(t)=1，则称该支集中的两个变迁为变迁对.

如图4所示，在PN1中，变迁t1、t2构成了变迁对.对应PN1的可达图如图4(b)所示，其构成了一个回路.

针对上述变迁对发生所产生的回路，可以通过抑制变迁t2发生来避免回路的产生.方法如下：若标识m0下变迁t1使能，且t1、t2对应一个变迁对，此时就标记变迁t2不使能，限制其在标识m1下发生，从而避免回路的产生.

特别地，若在任意标识m下，变迁对中的两个变迁均使能，则不对变迁对中的某个变迁进行抑制发生的处理.如图5所示，在标识m1下，变迁对中的两个变迁t1、t2均使能，此时若抑制变迁t2的发生会使得标识m3无法生成，进而影响求解的界数组的准确性，因此这种情况下不能抑制变迁t2的发生.

通过上述分析可以看到，通过定义变迁对及对变迁对进行处理，可以避免一部分可达图回路的产生，从而减少了生成可达图时需要存储的状态数目.

图4 Petri 网PN1 及其可达图Figure 4 Petri net PN1 and its reachability graph

图5 Petri 网PN2 及其可达图Figure 5 Petri net PN2 and its reachability graph

3.1.2 变迁环

定义13（变迁环）

设X为网PN 的一个T 不变量，满足若∀ti ∈PXP，∃tj,tk ∈PXP，，满足=•tj且•ti=，则称该支集为变迁环.

如图6所示，在图PN3中，变迁t1、t2、t3构成了变迁环.变迁t1的发生将库所p1中的托肯转移到库所p2中，变迁t2的发生将库所p2中的托肯转移到库所p3中，而变迁t3的发生又将库所p3中的托肯再次转移到库所p1中，对应PN3的可达图如图6(b)所示，m0、m1、m2构成了一个回路.

参考前述变迁对的处理方法并针对上述变迁环发生所产生的回路，可以通过抑制变迁t3发生来避免回路产生.方法如下：若标识m0下发生变迁t1产生标识m1，标识m1下发生变迁t2产生标识m2，且t1、t2、t3对应一个变迁环，通过对变迁环中已发生的变迁t1，t2进行计数处理，此时标记变迁t3不使能，限制其在标识m2下发生，从而避免回路产生.

图6 Petri 网PN3 及其可达图Figure 6 Petri net PN3 and its reachability graph

特别地，若在任意标识m下，变迁环中有2 个及以上变迁可以使能，则在该标识下，不对变迁环中某个变迁的发生进行计数处理.如图7所示，在标识m1下，变迁环{t1，t2，t3}中的2个变迁t1，t3均使能，此时若对变迁t1，t3的发生进行计数，则在标识m2下会抑制变迁t2发生，使标识m4无法生成，进而影响求解界的准确性，因此这种情况下对变迁t1，t3的发生进行不计数.同时，为了避免变迁环中计数处理的复杂化，若一个标识下能发生变迁环中的多个变迁，则在后续可达图生成过程中出现该变迁环时都不再进行消除变迁环的处理.

图7 Petri 网PN4 及其可达图Figure 7 Petri net PN4 and its reachability graph

3.2 求解算法

按照上述算法原理，本文算法在Petri 网可达状态生成中使用一个界数组bound[]来存储当前每个库所的最大托肯数，在遍历每个可达状态时，根据该状态中每个库所的托肯数更新界数组.对算法中的相关变量说明如下：M0为初始标识；visited[]为可达图生成过程中需要存储的标识集合，初始化为空；Uset为前文定义的尾变量变迁集合；disable[]为一个变迁集合，表示若某标识下能发生该集合中的变迁，则不再计算后续标识，初始化为空；circle[]为一个计数数组，表示变迁环中已发生变迁的个数，大小为Petri 网中变迁环的个数，初始化为0.

算法求解Petri 网中各库所界

输入：Petri 网(N,M0) ；网N的T 不变量

输出：各个库所的界bound[]∼bound[k]（k为Petri 网库所数目）

以图4所示的PN1为例进行算法运行演示如下：

对于m0下的使能变迁t1.第6 行判断t1对应变迁对{t1,t2}，且t2在m0下不使能；第7行t1不属于disable 集合，所以disable 集合中加入变迁t2；第15 行m0下发生t1得到m1，bound 数组由[1,1,0]更新为[1,1,1]；第16 行判断m1不属于visited 集合；第17 行由于Uset={t2}，而t1不属于Uset集合，所以visited 中不存储m1.

对于m1下的使能变迁t2.第6 行判断t2对应变迁对{t1,t2}，且t1在m1下不使能；第8行t2属于disable 集合，所以跳出本层for 循环.此时，由于不存在“新”结点，因此跳出while循环，算法结束.

对算法中的相关步骤解释说明如下：

第6 行，如前文所述，若标识m下的使能变迁同时包含1 个变迁对中的2 个变迁，则抑制某个变迁的产生会影响求解界数组的正确性，因此跳至15 行继续执行且后续使用Uset判断是否存储标识.第7 行，若变迁ti是变迁对中在时间顺序上先发生的变迁，则将变迁对中的另一个变迁放入集合disable 中.第8 行，若变迁ti对应一个变迁对且已经被放入集合disable中，则在标识m下不发生该变迁，达到了消除可达图中回路的目的.

第9∼14 行，若变迁环中变迁数目为s，则在发生了变迁环的s −1 个变迁后，抑制第s个变迁的发生，则不会再次产生之前状态，因此可以消除该回路.第10 行，若一个标识m下能发生变迁环中的多个变迁，对这些变迁进行计数会影响求解界数组的正确性，因此将circle数组中该变迁环所在的分量值记为–1，即之后若发生该变迁环中的变迁都不进行计数.第11行，若变迁环C还未发生s −1 个变迁时，则circle[C]加1，表示该变迁环中已发生变迁的个数加1.第12～14 行，若变迁ti对应的变迁环C已经发生了s −1 个变迁时，则第s个变迁ti使其不使能，同时计数数组置0，达到了消除可达图中回路的目的.

通过引入第6～14 行的方法，减少了可达图中回路数目，从而减少了可达图中需要存储的标识数目.举例来说，如图8和10 所示，若只用Uset判定，由于标识m2下发生集合Uset中的变迁t7能够产生标识m1则需存储标识m1，但用上述方法在标识m2下变迁t7不再使能，因此不需存储标识m1.

第15 行，生成一个新的标识并对界数组bound 进行更新.第16 行，若新标识已经存在于集合visited 中，说明该标识前已经产生过，则跳出本次循环.第17 行，m下发生变迁ti得到标识后，决定标识是否存储的依据是ti是否是Uset中的变迁.若一个标识不是由Uset中变迁发生得到的，则不会在集合visited 中存储这个状态，所以可能会再次生成该标识，并再次计算其使能变迁.由于不存储的状态不会构成一个回路，因此仍然能够保证可达图的终止.

可达图用以描述Petri 网的可达标识集，既与Petri 网的结构有关，还与Petri 网的初始标识有关.设可达图中标识数目为n，平均情况下每个标识的使能变迁数为d，同时在这一过程中，每产生一个标识需要判断是否已经产生过，消耗的时间为则传统可达图生成算法的时间复杂度为O(n2d).设本文算法变迁对、变迁环的数量为a，则与其相关的判断操作耗费的时间为an，所以本文算法的时间复杂度为O(n2d+n).

4 实例分析

选取模型检测比赛[8-9]（model checking contest）中的Petri 网模型ERK[10]，如图2所示，结合本文算法进行具体分析.

完全存储状态空间求取库所界的方法（Complete）[3]通过完全生成状态空间求解各个库所界，能够精确求解界以达到可达标识存储所需空间的最强压缩效果.但在此过程中，为了保证可达图生成的终止必须存储所有状态，因此需要耗费大量的空间资源.

使用P 不变量估计库所界的方法（P-inv）[4]通过求解Petri 网的P 不变量，结合状态方程估计库所界.但该方法无法保证得到精确的库所界，没有达到可达标识存储的最强压缩，因此浪费了部分空间.

与Complete 方法相比，本文提出的算法通过存储部分状态实现库所界的精确求解，无需存储全部状态空间，更有利于在复杂大规模系统中的应用.特别地，在可达图中回路较少甚至不存在回路的情况下，只需存储极少的状态数目甚至无需存储状态就能实现库所界的精确求解.与P-inv 方法相比，本文算法可以在覆盖所有库所的同时实现可达标识存储的最强压缩，提高压缩效果.

对图2所示的ERK 模型进行P 不变量估计的方法求库所界时，可以得到库所p1、p3、p4、p7,p8、p10、p11的界估计，即这些库所的界都为1.在后续可达标识存储时，这些库所的托肯值最大为1，所以可以采用位存储对这些库所使用1 bit 进行存储.但还有36%的库所由于不在P 不变量支集中而无法估计其界，所以对于这些库所的托肯值无法使用位压缩，仍需使用一个int 整型类型的存储空间（32 bit）进行存储，没有达到最强的压缩效果，还有进一步的提升空间.

采用存储部分状态空间的方法求解库所界如图8所示，若仅存储能发生在Uset集合中变迁的状态，虽然能够保证可达图的终止，但需要存储的状态（图8中灰色部分所示）占比整个状态空间为9/13=69%.

图8 状态空间——UsetFigure 8 State space—Uset

如图9所示，通过求解T不变量可以得到本例中变迁对为{t1,t2},{t3,t4},{t6,t7},{t9,t10}.

图9 T 不变量Figure 9 T invariant

通过消除变迁对的方法，如图10所示，本文的算法只需存储4 个状态（图10中灰色部分所示），占比整个状态空间减少至31%，即可求得库所精确界.求得该Petri 网所有库所界为1，因此每个标识中的每个库所的托肯数只需1 bit 来存储，比起之前32 bit 来存储，标识的存储空间压缩了32 倍.

图10 状态空间——本文算法Figure 10 State space—the proposed algorithm

随机选取了模型检测比赛的部分Petri 网模型，按照状态空间数目递增的模型顺序，将本文算法与完全生成状态空间求取库所界（Complete）、使用P不变量估计库所界（P-inv）两种方法进行对比，实验结果显示，本文算法在状态空间压缩方面效果较好，在一定程度上缓解了状态空间爆炸问题.另外，由于不同模型的空间消耗、标识大小差异较大，为了在同一个曲线图（图12空间消耗对比、图13标识压缩对比）中更加直观地呈现不同模型的实验效果，本文根据状态空间的大小将模型分成2组，分别呈现实验效果.

以下是第1 组模型的实验结果.

表1 第1 组模型Table 1 The first group models 个

覆盖率定义为能够求解估计界的库所数占所有库所数的比例；准确率定义为正确得到库所准确界的库所数占所有库所数的比例.表2和图11分别给出了P-inv 方法与本文算法对表1模型求解计算得到的覆盖率和准确率.

表2 库所覆盖率和界准确率对比表Table 2 Comparison of place coverage rate and bound accuracy rate %

图11 库所覆盖率和界准确率对比图Figure 11 Comparison of place coverage rate and bound accuracy rate

本文算法能够精确求解库所界，因此覆盖率和准确率都达到了100%.

Complete 空间为存储所有可达标识需要的空间；P-inv 空间为存储P不变量需要的空间；本文空间为存储T不变量及部分状态空间需要的空间.表3和图12分别给出了3 种方法对表1模型求解计算得到的空间消耗.

本文方法消耗空间介于Complete 和P-inv 两种方法之间，且比Complete 方法低得多.在model 9 中，可达图中不存在回路，无需存储状态空间也能保证可达图生成的正常终止，因此使用本文方法求解库所的界，空间消耗最低为0.

Complete 标识存储、P-inv 标识存储、本文方法标识存储分别为使用3 种方法求得库所界后，存储一个标识需要的空间.如model 1 的Complete 标识存储，共8 个库所，每个库所分配空间1 bit，所以表格中是1B.不压缩存储为不求取库所界，存储一个标识需要的空间.表4和图13分别给出了4 种方法对表1模型求解计算得到的标识存储空间.

表3 空间消耗对比表Table 3 Comparison of space consumption B

图12 空间消耗对比图Figure 12 Comparison of space consumption

表4 标识压缩对比表Table 4 Comparison of marking compression B

图13 标识压缩对比Figure 13 Comparison of marking compression

本文方法和Complete 方法求得了库所的精确界，因此都达到了库所最强压缩的效果.以下是第2 组模型的实验结果.

表5 第2 组模型Table 5 The second group models

表6给出了P-inv 方法和本文方法对表5模型求解计算得到的覆盖率和准确率.

表6 库所覆盖率和界准确率对比表Table 6 Comparison of place coverage rate and bound accuracy rate %

本文算法能够精确求解库所界，因此覆盖率和准确率都达到了100%.表7和图14给出了3 种方法对表5模型求解计算得到的空间消耗.在状态空间数目较大的情况下，存储T 不变量、P 不变量所耗费的空间几乎可以忽略不计.而消耗的这些空间对于提升求解得到的库所界的准确性是十分有效的.

表8和图15分别给出了Complete、P-inv、本文方法、不压缩存储等4 种方法对于表5模型求解计算得到的标识存储空间.

表7 空间消耗对比表Table 7 Comparison of space consumption MB

图14 空间消耗对比图Figure 14 Comparison of space consumption

表8 标识压缩对比表Table 8 Comparison of marking compression B

图15 标识压缩对比图Figure 15 Comparison of marking compression

本文方法和Complete 方法由于求得了库所的精确界，因此都达到了库所最强压缩的效果.表9及图16对比了三种方法求取库所界消耗的时间.

表9 三种方法求取库所界耗费的时间对比表Table 9 Time comparison of three methods to get place bound s

图16 三种方法求取库所界耗费的时间对比图Figure 16 Time comparison of three methods to get place bound

本文算法通过存储部分状态空间求得了库所的精确界，但由于只存储部分状态会有一部分未被存储的状态反复产生，与Complete 方法相比，耗费的时间更多.

在实验结果中部分模型消耗的时间比Complete 方法少，其原因为每当生成一个标识时，需要判断该标识之前是否产生过，这就需要与已经存储的标识集合visited 进行对比.在Complete 方法中，visited 中存储的是当前生成的全部可达标识.而在本文算法中，visited 中存储的是当前生成的部分可达标识，因此本文算法在实验过程中耗费的时间更少.

在model 6、model 8、model 10 中，由于没有存储全部可达标识，导致部分标识反复产生，因此本文方法比Complete 方法和P-inv 方法耗费的时间多，但在空间资源紧张的情况下，这种时间代价是值得的.

5 结 语

在Petri 网的众多性质中，由于Petri 网的有界性反映了被模拟系统运行过程中对有关资源的容量要求，因此受到广泛关注.但目前精确求解库所界的方法需要存储整个状态空间，给系统的内存资源带来了巨大挑战.本文提出了一种新的求解库所界的算法，与现有方法相比，本文算法结合了T 不变量的性质及引导消除可达图中的部分回路，减少了求解过程中所需的内存资源，实验结果验证了这一结论.

未来工作将注重于该算法在模型检测方面的应用.一方面，将结合on-the-fly 方法、对称约简、偏序约简等多种方法来进一步减少模型检测过程中消耗的时间、空间资源；另一方面，将深入思考在求库所界的过程中能否得到更多有效信息来提高模型检测的效率.