Abstract
Most specific characteristics of (Place/Transition) Petri nets can be traced back to a few basic features including the monotonicity of the enabling condition, the linearity of the firing rule, and the locality of both. These features enable “Petri net” analysis techniques such as the invariant calculus, the coverability graph technique, approaches based on unfolding, or structural (such as siphon/trap based) analysis. In addition, most verification techniques developed outside the realm of Petri nets can be applied to Petri nets as well.
In this paper, we want to demonstrate that the basic features of Petri nets do not only lead to additional analysis techniques, but as well to improved implementations of formalism-independent techniques. As an example, we discuss the explicit generation of a state space. We underline our arguments with some experience from the implementation and use of the Petri net based state space tool LoLA.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Berthelot, G.: Checking properties of nets using transformations. Advances in Petri Nets, pp. 19–40 (1986)
Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: On well–formed colored nets and their symbolic reachability graph. In: Proc. ICATPN, pp. 378–410 (1990)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronisation skeletons using brnaching tim temporal logic. In: Logic of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)
Christensen, S., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 450–464. Springer, Heidelberg (2001)
Commoner, F.: Deadlocks in Petri nets. Technical report, Applied Data Research Inc. Wakefield, Massachussetts (1972)
Curbera, F., et al.: Business process execution language for web services, version 1.1. Technical report, BEA, IBM, Microsoft (2003)
Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Proc. IEEE Int. Conf. Computer Design: VLSI in Computers and Processors, pp. 522–525. IEEE Computer Society Press, Los Alamitos (1992)
Emerson, E.A.: Handbook of Theoretical Computer Science, Ch. 16. Elsevier, Amsterdam (1990)
Esparza, J.: Model checking using net unfoldings. Technical Report 14/92, Universität Hildesheim (1992)
Finkel, A.: A minimal coverability graph for Petri nets. In: Proc. ICATPN, pp. 1–21 (1990)
Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model checking. In: Symp. on the Theory of Computing and Systems, pp. 130–140. IEEE Computer Society Press, Los Alamitos (1995)
Genrich, H., Lautenbach, K.: S–invariance in Pr/T–nets. Informatik–Fachberichte 66, 98–111 (1983)
Godefroid, P., Wolper, P.: A partial approach to model checking. In: IEEE Symp. on Logic in Computer Science, pp. 406–415 (1991)
Holzmann, G.: Design an Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
Hinz, S., Schmidt, K., Stahl, C.: Transforming BPEL to Petri nets. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds.) BPM 2005. LNCS, vol. 3649, pp. 220–235. Springer, Heidelberg (2005)
Jensen, K.: Coloured Petri nets and the invariant method. Theoretical Computer Science 14, 317–336 (1981)
Junttila, T.: New canonical representative marking algorithms for place/transition nets. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 258–277. Springer, Heidelberg (2004)
Karp, R.M., Miller, R.E.: Parallel programm schemata. Journ. Computer and System Sciences 4, 147–195 (1969)
Kristensen, L.M., Mailund, T.: A generalized sweep-line method for safety properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 549–567. Springer, Heidelberg (2002)
Kordon, F., Paviot-Adet, E.: Using CPN-AMI to validate a sfae channel protocol. In: Donatelli, S., Kleijn, J.H.C.M. (eds.) ICATPN 1999. LNCS, vol. 1639, Springer, Heidelberg (1999)
Kristensen, L., Schmidt, K., Valmari, A.: Question-guided stubborn set methods for state properties. Formal Methods in System Design 29(3), 215–251 (2006)
Krisensen, L.M., Valmari, A.: Improved question-guided stubborn set methods for state properties. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 282–302. Springer, Heidelberg (2000)
Kindler, E., Weber, M.: The Petri net kernel - an infrastructure for building petri net tools. STTT 3(4), 486–497 (2001)
Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structure and state-space reduction. In: Proc. IEEE Real-Time Systems Symp., pp. 14–24. IEEE Computer Society Press, Los Alamitos (1997)
Lautenbach, K., Schmidt, H.A.: Use of Petri nets for proving correctness of concurrent process systems. In: IFIP Congress, pp. 187–191 (1974)
McMillan, K.: The SMV homepage. http://www.cad.eecs.berkeley.edu/~kenmcmil/smv/
Mailund, T.: Sweeping the State Space - a sweep-line state space exploration method. PhD thesis, University of Aarhus (2003)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems (Specification), vol. 1. Springer, Heidelberg (1992)
McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronious circuits. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 164–177. Springer, Heidelberg (1993)
Peled, D.: All from one, one for all: on model–checking using representitives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)
Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
Roch, S., Starke, P.: INA Integrierter Netz Analysator Version 2.1. Technical Report 102, Humboldt–Universität zu Berlin (1998)
Schmidt, K.: Stubborn set for standard properties. In: Donatelli, S., Kleijn, J.H.C.M. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 46–65. Springer, Heidelberg (1999)
Schmidt, K.: How to calculate symmetries of Petri nets. Acta Informatica 36, 545–590 (2000)
Schmidt, K.: Integrating low level symmetries into reachability analysis. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol. 1785, pp. 315–331. Springer, Heidelberg (2000)
Schmidt, K.: LoLA – a low level analyzer. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 465–474. Springer, Heidelberg (2000)
Schmidt, K.: Stubborn set for modelchecking the EF/AG fragment of CTL. Fundamenta Informaticae 43(1-4), 331–341 (2000)
Schmidt, K.: Using Petri net invariantsin state space construction. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 473–488. Springer, Heidelberg (2003)
Schmidt, K.: Automated generation of a progress measure for the sweep-line method. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 192–204. Springer, Heidelberg (2004)
Schröter, C., Schwoon, S., Esparza, J.: The Model-Checking Kit. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 463–472. Springer, Heidelberg (2003)
Stahl, C., Reisig, W., Krstic, M.: Hazard detection in a GALS wrapper: A case study. In: Proc. ACSD, pp. 234–243 (2005)
Starke, P.: Reachability analysis of Petri nets using symmetries. J. Syst. Anal. Model. Simul. 8, 294–303 (1991)
Talcott, C.: Personal communication. Dagstuhl Seminar (2007)
Reisig, W., et al.: The homepage of the project Tools4BPEL. http://www2.informatik.hu-berlin.de/top/forschung/projekte/tools4bpel/
Valmari, A.: Error detection by reduced reachability graph generation. ICATPN (1988)
Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Advances in Petri Nets 1990. LNCS, vol. 483, pp. 491–511. Springer, Heidelberg (1991)
Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 59–70. Springer, Heidelberg (1993)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Wolf, K. (2007). Generating Petri Net State Spaces. In: Kleijn, J., Yakovlev, A. (eds) Petri Nets and Other Models of Concurrency – ICATPN 2007. ICATPN 2007. Lecture Notes in Computer Science, vol 4546. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73094-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-73094-1_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73093-4
Online ISBN: 978-3-540-73094-1
eBook Packages: Computer ScienceComputer Science (R0)