This Article 
 Bibliographic References 
 Add to: 
Symbolic Analysis of Bounded Petri Nets
May 2001 (vol. 50 no. 5)
pp. 432-448

Abstract—This work presents a symbolic approach for the analysis of bounded Petri nets. The structure and behavior of the Petri net is symbolically modeled by using Boolean functions, thus reducing reasoning about Petri nets to Boolean calculation. The set of reachable markings is calculated by symbolically firing the transitions in the Petri net. Highly concurrent systems suffer from the state explosion problem produced by an exponential increase of the number of reachable states. This state explosion is handled by using Binary Decision Diagrams (BDDs) which are capable of representing large sets of markings with small data structures. Petri nets have the ability to model a large variety of systems and the flexibility to describe causality, concurrency, and conditional relations. The manipulation of vast state spaces generated by Petri nets enables the efficient analysis of a wide range of problems, e.g., deadlock freeness, liveness, and concurrency. A number of examples are presented in order to show how large reachability sets can be generated, represented, and analyzed with moderate BDD sizes. By using this symbolic framework, properties requiring an exhaustive analysis of the reachability graph can be efficiently verified.

[1] F.M. Brown, Boolean Reasoning: The Logic of Boolean Equations. Kluwer Academic, 1990.
[2] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams," ACM Computing Surveys, vol., 24 no. 3, pp. 293-318, 1992.
[3] J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, "Symbolic Model Checking: 1020States and Beyond," Proc. IEEE Symp. Logic in Computer Science, pp. 428-439, 1990.
[4] J.M. Colom and M. Silva, “Improving the Linearly Based Characterization of P/T Nets,” Proc. Advances in Petri Nets 1990, G. Rozenberg, ed., pp. 113-145, 1991.
[5] O. Coudert, C. Berthet, and J.C. Madre, “Verification of Sequential Machines Using Boolean Functional Vectors,” Proc. IFIP Int'l Workshop Applied Formal Methods for Correct VLSI Design, pp. 111-128, Nov. 1989.
[6] O. Coudert, C. Berthet, and J.C. Madre, “Formal Boolean Manipulations for the Verification of Sequential Machines,” Proc. European Conf. Design Automation (EDAC), pp. 57-61, Mar. 1990.
[7] K. Hamaguchi, H. Hiraishi, and S. Yajima, “Design Verification of Asynchronous Sequential Circuits Using Symbolic Model Checking,” Proc. Int'l Symp. Logic Synthesis and Microprocessor Architecture, pp. 84-90, July 1992.
[8] Y. Matsunaga, P.C. McGeer, and R.K. Brayton, “On Computing the Transitive Closure of a State Transition Relation,” Proc. ACM/IEEE Design Automation Conf., pp. 260-265, June 1993.
[9] T. Murata, “Petri Nets: Properties, Analysis and Application,” Proc. IEEE, vol. 77, no. 4, 1989.
[10] E. Pastor et al., "Petri Net Analysis Using Boolean Manipulation," Proc. Int'l Conf. Applications and Theory of Petri Nets, LNCS 815, Springer-Verlag, Berlin, 1994, pp. 416-435.
[11] E. Pastor, J. Cortadella, and M.A. Peña, “Structural Methods to Improve the Symbolic Analysis of Petri Nets,” Proc. 20th Int'l Conf. Application and Theory of Petri Nets, pp. 26-45, June 1999.
[12] C.A. Petri, “Kommunikation mit Automaten,” PhD thesis, Bonn, Institut für Instrumentelle Mathematik, 1962 (technical report Schriften des IIM Nr. 3).
[13] W. Reisig, “Petri Nets—An Introduction,” EATCS Monographs on Theoretical Computer Science. Springer-Verlag, vol. 4, 1985.
[14] O. Roig, J. Cortadella, and E. Pastor, “Verification of Asynchronous Circuits by BDD-Based Model Checking of Petri Nets,” Proc. 16th Int'l Conf. Application and Theory of Petri Nets, pp. 374-391, June 1995.
[15] R. Rudell, "Dynamic Variable Ordering for Ordered Binary Decision Diagrams," Proc. ICCAD-93, pp. 42-47, 1993.
[16] A. Xie, S. Kim, and P.A. Beerel, “Bounding Average Time Separations of Events in Stochastic Timed Petri Nets with Choice,” Proc. Int'l Symp. Advanced Research in Asynchronous Circuits and Systems, pp. 94-107, Apr. 1999.
[17] A. Xie and P.A. Beerel, “Implicit Enumeration of Strongly Connected Components,” Proc. Int'l Conf. Computer-Aided Design, pp. 37-40, Nov. 1999.
[18] T. Yoneda, H. Hatori, A. Takahara, and S. Minato, “BDDs vs. Zero-Suppressed BDDs: For CTL Symbolic Model Checking of Petri Nets,” Proc. Formal Methods in Computer-Aided Design, pp. 435-449, 1996.

Index Terms:
Petri nets, formal verification, symbolic methods, Binary Decition Diagrams.
Enric Pastor, Jordi Cortadella, Oriol Roig, "Symbolic Analysis of Bounded Petri Nets," IEEE Transactions on Computers, vol. 50, no. 5, pp. 432-448, May 2001, doi:10.1109/12.926158
Usage of this product signifies your acceptance of the Terms of Use.