Petri网的展开图是一种特殊的并发系统状态空间搜索方法,它不需要重复考虑并发事件的所有可能的交集,从而大大缩减状态空间爆炸给验证分析带来的空间复杂度和时间复杂度。使用展开图分析Petri网的行为属性与传统的Petri网分析方法相比,具有自己的特点。该文首先介绍了Petri网展开图的构造算法,在此基础上使用展开图分析方法对一个典型Petri网的活性,有界性和可逆性等行为属性进行了分析,并与传统的Petri网分析方法作比较。
Unfolding of Petri nets is a special method for exploring the state space of concurrent systems, which excludes the possible intersection of concurrent events so as to greatly reduce the complexity degree of space and time from state space explosion. In contrast to the traditional analyzing method of Petri nets, the unfolding method has some merits. In this paper, an algorithm for constructing an unfolding of a Petri net is introduced at first, and then, some behavioral properties, such as liveness, boundedness and reversibility of a typical Petri net are analyzed with its unfolding. In conclusion, the comparison between traditional analyzing method and unfolding method of Petri nets is mentioned.