Chinese Journal of Computers   Full Text
Title	Symbolic Reachability Analysis of Petri Nets Using ZBDDs
Authors	.LI Feng-Ying1),2) GU Tian-Long2) XU Zhou-Bo1),2)
Address	1)(Electronic Engineering School, Xidian University, Xi’an 710071) 2)(School of Computer Science, Guilin University of Electronic Technology, Guilin, Guangxi 541004)
Year	2009
Issue	No.12(2420—2428)
Abstract &   Background	Abstract Petri net is a graph-based mathematical formalism suitable to model, analyze and control the behavior of discrete event concurrent systems. Reachability tree is one of typical techniques to analyze Petri nets. Highly concurrent systems often suffer from state combinatorial explosion problem which renders it very hard and even impossible to handle Petri nets using the reachability tree technique. Fortunately, the marking vectors or the state spaces of Petri nets are often very sparse, and Zero-Suppressed Binary Decision Diagram (ZBDD) is a novel data structure and efficient way to represent and manipulate 0-1 sparse vectors. The authors developed the novel ZBDD-based symbolic technique to formulate, generated and manipulated the reachability marking vectors，thus the performance of Petri nets could be evaluated symbolically. The experimental results show that the symbolic technique can handle large-scale Petri nets more efficiently and compactly. Keywords Petri net; Zero-suppressed binary decision diagram; Background This work is supported by the National Natural Science Foundations of China (60963010,60903079). Petri nets are a graphical and mathematical formalism to model and analyze the behavior of discrete event concurrent systems, the state space of which is a set consisting of sparse vectors. But analyzing Petri nets often suffer from state combinational problem that renders it very difficult and even impossible to handle large-scale Petri nets. The existing methods for the analysis of Petri nets, such as reachability tree methods, enumerative methods, matrix-equation methods and reduction methods, have certain limitations respectively and can not overcome state explosion problem. OBDD is reported one of the most efficient symbolic technique and capable of representing large sets of markings with small data structures. ZBDD is a special type of OBDD for manipulating sets of vector combinations. The symbolic ZBDD analysis technology of Petri nets is discussed, and a symbolic ZBDD analysis algorithm for Petri nets is developed in this paper. The experimental results show that the symbolic ZBDD analysis technology can handle large-scale Petri nets, and ZBDDs are competitive for the symbolic analysis of Petri nets.