Abstract
Due to their appealing conceptual simplicity and availability of computer tools for their analysis, Petri nets are widely used to model discrete-event systems in many areas of engineering. However, the computational resources required to carry out the analysis of a Petri net model are often enormous, hindering their practical impact. In this survey, we consider how symbolic methods based on the use of decision diagrams can greatly increase the size of Petri nets that an ordinary computer can reasonably tackle. In particular, we present this survey from the perspective of the efficient saturation method we proposed a decade ago, and introduce along the way the most appropriate classes of decision diagrams to answer important Petri net questions, from reachability to CTL model checking and counterexample generation, from p-semiflow computation to the solution of timed or Markovian nets.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ajmone Marsan, M., Balbo, G., Conte, G.: A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Trans. Comp. Syst. 2(2), 93–122 (1984)
Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons (1995)
Baarir, S., Beccuti, M., Cerotti, D., De Pierro, M., Donatelli, S., Franceschinis, G.: The GreatSPN tool: recent enhancements. SIGMETRICS Perform. Eval. Rev. 36, 4–9 (2009)
Babar, J., Beccuti, M., Donatelli, S., Miner, A.S.: GreatSPN Enhanced with Decision Diagram Data Structures. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 308–317. Springer, Heidelberg (2010)
Babar, J., Miner, A.S.: Meddly: Multi-terminal and Edge-valued Decision Diagram LibrarY. In: Proc. QEST, pp. 195–196. IEEE Computer Society (2010)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking Without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)
Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comp. 45(9), 993–1002 (1996)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98, 142–170 (1992)
Çinlar, E.: Introduction to Stochastic Processes. Prentice-Hall (1975)
Ciardo, G.: Data Representation and Efficient Solution: A Decision Diagram Approach. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 371–394. Springer, Heidelberg (2007)
Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.: Logical and stochastic modeling with SMART. Perf. Eval. 63, 578–608 (2006)
Ciardo, G., Lüttgen, G., Siminiceanu, R.: Saturation: An Efficient Iteration Strategy for Symbolic State Space Generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328–342. Springer, Heidelberg (2001)
Ciardo, G., Lüttgen, G., Yu, A.J.: Improving Static Variable Orders Via Invariants. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 83–103. Springer, Heidelberg (2007)
Ciardo, G., Marmorstein, R., Siminiceanu, R.: The saturation algorithm for symbolic state space exploration. Software Tools for Technology Transfer 8(1), 4–25 (2006)
Ciardo, G., Mecham, G., Paviot-Adet, E., Wan, M.: P-semiflow Computation with Decision Diagrams. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 143–162. Springer, Heidelberg (2009)
Ciardo, G., Miner, A.S.: A data structure for the efficient Kronecker solution of GSPNs. In: Proc. PNPM, pp. 22–31. IEEE Comp. Soc. Press (1999)
Ciardo, G., Muppala, J.K., Trivedi, K.S.: On the solution of GSPN reward models. Perf. Eval. 12(4), 237–253 (1991)
Ciardo, G., Siminiceanu, R.: Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest Paths. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 256–273. Springer, Heidelberg (2002)
Ciardo, G., Trivedi, K.S.: A decomposition approach for stochastic reward net models. Perf. Eval. 18(1), 37–59 (1993)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: An Open Source Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Clarke, E., Fujita, M., McGeer, P.C., Yang, J.C.-Y., Zhao, X.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. In: IWLS 1993 International Workshop on Logic Synthesis (May 1993)
Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Clarke, E.M., Wing, J.M., Alur, R., Cleaveland, R., Dill, D., Emerson, A., Garland, S., German, S., Guttag, J., Hall, A., Henzinger, T., Holzmann, G., Jones, C., Kurshan, R., Leveson, N., McMillan, K., Moore, J., Peled, D., Pnueli, A., Rushby, J., Shankar, N., Sifakis, J., Sistla, P., Steffen, B., Wolper, P., Woodcock, J., Zave, P.: Formal methods: state of the art and future directions. ACM Comp. Surv. 28(4), 626–643 (1996)
Donatelli, S.: Superposed Generalized Stochastic Petri Nets: Definition and Efficient Solution. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 258–277. Springer, Heidelberg (1994)
Farkas, J.: Theorie der einfachen ungleichungen. Journal für die reine und andgewandte Mathematik 124, 1–27 (1902)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: Cadp 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)
Graf, S., Steffen, B., Lüttgen, G.: Compositional minimisation of finite state systems using interface specifications. Journal of Formal Aspects of Computing 8(5), 607–616 (1996)
Grassmann, W.K.: Finding transient solutions in Markovian event systems through randomization. In: Numerical Solution of Markov Chains, pp. 357–371. Marcel Dekker, Inc. (1991)
Heljanko, K.: Bounded Reachability Checking with Process Semantics. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 218–232. Springer, Heidelberg (2001)
Heljanko, K., Niemelä, I.: Answer set programming and bounded model checking. In: Answer Set Programming (2001)
Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. In: 22th Annual Symp. on Foundations of Computer Science, pp. 150–158. IEEE Comp. Soc. Press (1981)
McMillan, K.L.: The SMV system, symbolic model checking - an approach. Technical Report CMU-CS-92-131, Carnegie Mellon University (1992)
Kam, T., Villa, T., Brayton, R.K., Sangiovanni-Vincentelli, A.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic 4(1-2), 9–62 (1998)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 52–66. Springer, Heidelberg (2003)
Lai, Y.-T., Pedram, M., Vrudhula, B.K.: Formal verification using edge-valued binary decision diagrams. IEEE Trans. Comp. 45, 247–255 (1996)
Lampka, K., Siegle, M.: MTBDD-based activity-local state graph generation. In: Proc. PMCCS, pp. 15–18 (September 2003)
McMillan, K.L.: Symbolic Model Checking. Kluwer (1993)
Merlin, P.M.: A study of the recoverability of computing systems. PhD thesis, Department of Information and Computer Science, University of California, Irvine (1974)
Miner, A.S.: Efficient state space generation of GSPNs using decision diagrams. In: Proc. DSN, pp. 637–646 (June 2002)
Ogata, S., Tsuchiya, T., Kikuno, T.: SAT-Based Verification of Safe Petri Nets. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 79–92. Springer, Heidelberg (2004)
Pastor, E., Roig, O., Cortadella, J., Badia, R.M.: Petri Net Analysis using Boolean Manipulation. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 416–435. Springer, Heidelberg (1994)
Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice-Hall (1981)
Petri, C.: Kommunikation mit Automaten. PhD thesis, University of Bonn (1962)
Reisig, W.: Elements of Distributed Algorithms (Modeling and Analysis with Petri Nets. Springer, Heidelberg (1998)
Roig, O., Cortadella, J., Pastor, E.: Verification of Asynchronous Circuits by BDD-Based Model Checking of Petri Nets. In: DeMichelis, G., Díaz, M. (eds.) ICATPN 1995. LNCS, vol. 935, pp. 374–391. Springer, Heidelberg (1995)
Siminiceanu, R., Ciardo, G.: New Metrics for Static Variable Ordering in Decision Diagrams. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 90–104. Springer, Heidelberg (2006)
Somenzi, F.: CUDD: CU Decision Diagram Package, Release 2.4.2, http://vlsi.colorado.edu/~fabio/CUDD/
Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press (1994)
Tilgner, M., Takahashi, Y., Ciardo, G.: SNS 1.0: Synchronized Network Solver. In: 1st Int. Workshop on Manufacturing and Petri Nets, pp. 215–234 (June 1996)
Valmari, A.: A Stubborn Attack on the State Explosion Problem. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 156–165. Springer, Heidelberg (1992)
Wan, M., Ciardo, G.: Symbolic Reachability Analysis of Integer Timed Petri Nets. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tůma, P., Valencia, F. (eds.) SOFSEM 2009. LNCS, vol. 5404, pp. 595–608. Springer, Heidelberg (2009)
Wan, M., Ciardo, G., Miner, A.S.: Approximate steady-state analysis of large Markov models based on the structure of their decision diagram encoding. Perf. Eval. 68, 463–486 (2011)
Yoneda, T., Hatori, H., Takahara, A., Minato, S.-I.: BDDs vs. Zero-Suppressed BDDs: For CTL Symbolic Model Checking of Petri Nets. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 435–449. Springer, Heidelberg (1996)
Yu, A.J., Ciardo, G., Lüttgen, G.: Decision-diagram-based techniques for bounded reachability checking of asynchronous systems. Software Tools for Technology Transfer 11(2), 117–131 (2009)
Zhao, Y., Ciardo, G.: Symbolic CTL Model Checking of Asynchronous Systems using Constrained Saturation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 368–381. Springer, Heidelberg (2009)
Zuberek, W.L.: Timed Petri nets definitions, properties, and applications. Microelectronics and Reliability 31, 627–644 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Ciardo, G., Zhao, Y., Jin, X. (2012). Ten Years of Saturation: A Petri Net Perspective. In: Jensen, K., Donatelli, S., Kleijn, J. (eds) Transactions on Petri Nets and Other Models of Concurrency V. Lecture Notes in Computer Science, vol 6900. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29072-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-29072-5_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29071-8
Online ISBN: 978-3-642-29072-5
eBook Packages: Computer ScienceComputer Science (R0)