Abstract
Downward closures of Petri net reachability sets can be finitely represented by their set of maximal elements called the minimal coverability set or Clover. Many properties (coverability, boundedness, ...) can be decided using Clover, in a time proportional to the size of Clover. So it is crucial to design algorithms that compute it efficiently. We present a simple modification of the original but incomplete Minimal Coverability Tree algorithm (MCT), computing Clover, which makes it complete: it memorizes accelerations and fires them as ordinary transitions. Contrary to the other alternative algorithms for which no bound on the size of the required additional memory is known, we establish that the additional space of our algorithm is at most doubly exponential. Furthermore we have implemented a prototype MinCov which is already very competitive: on benchmarks it uses less space than all the other tools and its execution time is close to the one of the fastest tool.
The work was carried out in the framework of ReLaX, UMI2000 and also supported by ANR-17-CE40-0028 project BRAVAS.
Chapter PDF
Similar content being viewed by others
Keywords
References
Blockelet, M., Schmitz, S.: Model checking coverability graphs of vector addition systems. In: Proceedings of MFCS 2011. LNCS, vol. 6907, pp. 108–119 (2011)
Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously. In: Proceedings of TACAS 2016. LNCS, vol. 9636, pp. 480–496. Springer (2016)
Blondin, M., Finkel, A., McKenzie, P.: Well behaved transition systems. Logical Methods in Computer Science 13(3), 1–19 (2017)
Demri, S.: On selective unboundedness of VASS. J. Comput. Syst. Sci. 79(5), 689–713 (2013)
Finkel, A.: Reduction and covering of infinite reachability trees. Information and Computation 89(2), 144–179 (1990)
Finkel, A.: The minimal coverability graph for Petri nets. In: Advances in Petri Nets. LNCS, vol. 674, pp. 210–243 (1993)
Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part II: Complete WSTS. Logical Methods in Computer Science 8(4), 1–35 (2012)
Finkel, A., Geeraerts, G., Raskin, J.F., Van Begin, L.: A counter-example to the minimal coverability tree algorithm. Tech. rep., Université Libre de Bruxelles, Belgium (2005), http://www.lsv.fr/Publis/PAPERS/PDF/FGRV-ulb05.pdf
Finkel, A., Haddad, S., Khmelnitsky, I.: Minimal coverability tree construction made complete and efficient (2020), https://hal.inria.fr/hal-02479879
Geeraerts, G., Raskin, J.F., Van Begin, L.: On the efficient computation of the minimal coverability set of Petri nets. International Journal of Fundamental Computer Science 21(2), 135–165 (2010)
Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)
Leroux, J.: Distance between mutually reachable Petri net configurations (Jun 2019), https://hal.archives-ouvertes.fr/hal-02156549, preprint
Piipponen, A., Valmari, A.: Constructing minimal coverability sets. Fundamenta Informaticae 143(3–4), 393–414 (2016)
Reynier, P.A., Servais, F.: Minimal coverability set for Petri nets: Karp and Miller algorithm with pruning. Fundamenta Informaticae 122(1–2), 1–30 (2013)
Reynier, P.A., Servais, F.: On the computation of the minimal coverability set of Petri nets. In: Proceedings of Reachability Problems 2019. LNCS, vol. 11674, pp. 164–177 (2019)
Valmari, A., Hansen, H.: Old and new algorithms for minimal coverability sets. Fundamenta Informaticae 131(1), 1–25 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Finkel, A., Haddad, S., Khmelnitsky, I. (2020). Minimal Coverability Tree Construction Made Complete and Efficient. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)