基于展开的状态空间搜索方法

文/王博　代飞　黄苾

Petri网是1962年由德国科学家Carl Adam Petri博士在他的博士论文《用自动机通信》中创立的一种网状结构。本质上，它是一个有向二分图，由库所和变迁组成。

可达图作为分析Petri网动态性质的一种重要分析技术，被大量广泛使用。但是，基于可达图的状态空间搜索方法需要考虑并发事件间所有的交织可能，进而导致状态空爆炸。也就是说，使用基于可达图的状态空间搜索方法对并发系统进行分析时，常常面临效率低下的问题。

针对上述问题，McMillan在1995提出了展开（unfolding）的概念。与基于可达图的状态空间搜索方法相比，基于展开的状态空间搜索方法不需要考虑并发事件间的所有可能交织，可避免状态空间爆炸。本文将给出展开Petri网的算法，通过一个例子，直观比较可达图和出现网（Occurrence Net，由展开Petri网得到）的规模。

图1：一个Petri网

图2：可达图

1　Petri网的可达图和出现网

定义1（Petri网）Petri网是一个四元组∑=(P, T; F, M)，其中：

（4） 映 射 M：P→ {0, 1, 2, 3...}称 为Petri网的一个标识。通常用M0表示Petri网的初始标识。

通常，库所使用圆圈表示，变迁使用方框表示，流关系使用有向线段表示，托肯使用实心小黑点表示。

定义2（可达标识集）设∑=(P, T; F, M0)是一个Petri网，其中M0是初始情态。S的可达标识集R(M0)为满足下面条件的最小集合：

（1）M0∈ R(M0)；

（2）若M∈R(M0)，且存在t∈T，使得M[t＞M’，则M’∈R(M0)。

可达标识集R(M0)描述了∑所有可能的状态。若以R(M0)中的元素为节点，有向弧描述标识间的后继关系，可构造出∑的可达图。

定义3（可达图）设∑=(P, T; F, M0)是Petri网，其中M0是初始情态。∑的可达图定义为一个三元组RG(Σ)=(R(M0), E, Tran)，其中：

（1）E={(Mi, Mj)|Mi, Mj∈ R(M0),tk∈ T:Mi[tk＞Mj}；

（2） 映 射Tran:E→T称 为 迁 移，Tran(Mi, Mj)=tk当且仅当 Mi[tk＞Mj；

称 R(M0)为 RG(Σ)的顶点集，E 为 RG(Σ)的弧集。若Tran(Mi, Mj)=tk，称tk为弧(Mi, Mj)的旁标，通常，将其记为

定义4（出现网）设Σ=(P, T; F, M0)是一个Petri网，Σ的展开是一个出现网O=(P', T', F';L)，其中:

（1）L：P'∪T'→P∪T是标号函数，用于建立P'到P及T'到T的映射，通常称P'为条件集，T'为事件集，：

图3：出现网

2　展开Petri网的算法

对于任意给定的一个Petri网，可由算法1构造得到出现网。

算法1 展开Petri网。

输入：任意一个Petri网是Σ=(P, T; F, M)；

输出：该Petri网的出现网O=(P', T', F'; L)。

（1）将Petri网中每一个初始托肯所在的库所复制到出现网中；

（2）从Petri网中选择一个变迁t；

（3）对于·t中的每个库所，在出现网中寻找其副本，如果无法找到，返回步骤2。对于一个变迁，不要两次选择相同的库所子集；

（4）如果被选中的一对库所是冲突关系或者有前后关系（即它们不是并发的），则返回步骤2；

（5）将t复制到出现网中，称为t'。从步骤3中找到的每个库所画一条弧到t'；

（6）对于t·中的每个库所，将其复制到出现网中，并从t'画一条弧到这些库所；

（7）无限地重复步骤2～6。

如上所述，算法1构造的出现网是一个无限网，它在保持Petri网中的各变迁间的关系（顺序、冲突、并发等）的同时，表示了网内所有托肯的转移过程。

3　例子

下面通过一个例子，来直观比较可达图和出现网的规模。

图1所示的是一个Petri网。在Petri网存在多个变迁间的并发关系，例如变迁t1和t2，变迁t2和t3，变迁t1和t3，变迁t1和t5等。

图2是使用开源工具PIPE 4.3生成的图1所示Petri网的可达图截图。

从图2可以看出：图1所示Petri网对应的可达图有29个状态，在图2中用椭圆表示。其中，状态s1-s27刻画了并发变迁产生的状态迁移关系。进一步分析，不难看出：随着Petri网中并发变迁的数量增加，可达图中的状态呈指数增长，不可避免地会出现状态空间爆炸。

图3是根据算法1生成的图1所示Petri网的出现网。其中，p0-1表示原Petri网中库所p0在出现网的生成次序；t0-1表示原Petri网中变迁t0在出现网的生成次序。

对比图2和图3，可以看出：图3所示出现网的规模远远小于图2所示可达图的规模。由此可以说明：基于展开的状态空间搜索方法可避免状态空间爆炸问题

4　总结

通过一个例子，直观对比了基于展开的状态空间搜索方法和基于可达图的状态空间搜索方法，以说明基于展开的状态空间搜索方法可避免状态空间爆炸问题。