Abstract
We propose a method to count the number of reachable markings of a Petri net without having to enumerate these first. The method relies on a structural reduction system that reduces the number of places and transitions of the net in such a way that we can faithfully compute the number of reachable markings of the original net from the reduced net and the reduction history. The method has been implemented and computing experiments show that reductions are effective on a large benchmark of models.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Behle, M., Eisenbrand, F.: 0/1 vertex and facet enumeration with BDDs. In: 9th Workshop on Algorithm Engineering and Experiments. SIAM (2007)
Berthelot, G.: Checking properties of nets using transformations. In: Rozenberg, G. (ed.) APN 1985. LNCS, vol. 222, pp. 19–40. Springer, Heidelberg (1986). https://doi.org/10.1007/BFb0016204
Berthelot, G.: Transformations and decompositions of nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 254, pp. 359–376. Springer, Heidelberg (1987). https://doi.org/10.1007/978-3-540-47919-2_13
Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA-construction of abstract state spaces for Petri nets and Time Petri nets. Int. J. Prod. Res. 42(14), 2741–2756 (2004)
Esparza, J., Schröter, C.: Net reductions for LTL model-checking. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 310–324. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44798-9_25
Kordon, F., et al.: Complete Results for the 2017 Edition of the Model Checking Contest, June 2017. http://mcc.lip6.fr/
Kordon, F., Garavel, H., Hillah, L.M., Paviot-Adet, E., Jezequel, L., Rodríguez, C., Hulin-Hubard, F.: MCC’2015–the fifth model checking contest. In: Koutny M., Desel J., Kleijn J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol 9930, pp. 262–273. Springer, Heidelberg (2016)
Hack, M.: Decidability questions for Petri Nets. Ph.D. thesis, Massachusetts Institute of Technology (1976)
Hillah, L.M., Kordon, F.: Petri nets repository: a tool to benchmark and debug petri net tools. In: van der Aalst, W., Best, E. (eds.) PETRI NETS 2017. LNCS, vol. 10258, pp. 125–135. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57861-3_9
Jensen, J.F., Nielsen, T., Oestergaard, L.K., Srba, J.: TAPAAL and reachability analysis of P/T nets. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 307–318. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53401-4_16
Levy, F.K., Thompson, G.L., Wiest, J.D.: Introduction to the Critical-Path Method. Industrial Scheduling. Prentice-Hall, Englewood Cliffs (1963)
De Loera, J.A., Hemmecke, R., Köppe, M.: Algebraic and Geometric Ideas in the Theory of Discrete Optimization. SIAM, Philadelphia (2013)
De Loera, J.A., Hemmecke, R., Tauzer, J., Yoshida, R.: Effective lattice point counting in rational convex polytopes. J. Symbolic Comput. 38(4), 1273–1302 (2004)
Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice Hall PTR, Upper Saddle River (1981)
Recalde, L., Teruel, E., Silva, M.: Improving the decision power of rank theorems. In: 1997 IEEE International Conference on Systems, Man, and Cybernetics. Computational Cybernetics and Simulation, vol. 4, pp. 3768–3773 (1997)
Schmidt, K.: Using petri net invariants in state space construction. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 473–488. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X_35
Silva, M., Terue, E., Colom, J.M.: Linear algebraic and linear programming techniques for the analysis of place/transition net systems. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 309–373. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-65306-6_19
Stahl, C.: Decomposing petri net state spaces. In: 18th German Workshop on Algorithms and Tools for Petri Nets (AWPN 2011), Hagen, Germany, September 2011
Thierry-Mieg, Y., Poitrenaud, D., Hamez, A., Kordon, F.: Hierarchical set decision diagrams and regular models. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 1–15. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_1
Wolf, K.: Generating petri net state spaces. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 29–42. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73094-1_5
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Berthomieu, B., Le Botlan, D., Dal Zilio, S. (2018). Petri Net Reductions for Counting Markings. In: Gallardo, M., Merino, P. (eds) Model Checking Software. SPIN 2018. Lecture Notes in Computer Science(), vol 10869. Springer, Cham. https://doi.org/10.1007/978-3-319-94111-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-94111-0_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94110-3
Online ISBN: 978-3-319-94111-0
eBook Packages: Computer ScienceComputer Science (R0)