Abstract
The verification of infinite-state systems is a challenging task. A prominent instance is reachability analysis of Petri nets, for which no efficient algorithm is known. The minimal coverability set of a Petri net can be understood as an approximation of its reachability set described by means of \(\omega \)-markings (i.e. markings in which some entries may be set to infinity). It allows to solve numerous decision problems on Petri nets, such as any coverability problem. In this paper, we study the computation of the minimal coverability set.
This set can be computed using the Karp and Miller trees, which perform accelerations of cycles along branches [10]. The resulting algorithm may however perform redundant computations. In a previous work [17], we proposed an improved algorithm allowing pruning between branches of the Karp and Miller tree, and proved its correctness. The proof of its correctness was complicated, as the introduction of pruning between branches may yield to incompleteness issues [5, 9].
In this paper, we propose a new proof of the correctness of our algorithm. This new proof relies on an original invariant of the algorithm, leading to the following assets:
-
1.
it is considerably shorter and simpler,
-
2.
it allows to prove the correctness of a more generic algorithm, as the acceleration used is let as a parameter. Indeed, we identify the property that the acceleration should satisfy to ensure completeness.
-
3.
it opens the way to a generalization of our algorithm to extensions of Petri nets.
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
Blondin, M., Finkel, A., Goubault-Larrecq, J.: Forward analysis for wsts, part III: Karp-Miller trees. In: 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, vol. 93 of LIPIcs, pp. 16:1–16:15. Leibniz-Zentrum fuer Informatik (2017)
Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 480–496. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_28
Cardoza, E., Lipton, R.J., Meyer, A.R.: Exponential space complete problems for petri nets and commutative semigroups: preliminary report. In: Proceedings of the 8th Annual ACM Symposium on Theory of Computing, Hershey, Pennsylvania, USA, 3–5 May 1976, pp. 50–54. ACM (1976)
Finkel, A.: A generalization of the procedure of Karp and Miller to well structured transition systems. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 499–508. Springer, Heidelberg (1987). https://doi.org/10.1007/3-540-18088-5_43
Finkel, A.: The minimal coverability graph for Petri nets. In: Rozenberg, G. (ed.) ICATPN 1991. LNCS, vol. 674, pp. 210–243. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56689-9_45
Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part I: completions. In: Proceedings of STACS 2009, vol. 3 of LIPIcs, pp. 433–444. Leibniz-Zentrum für Informatik (2009)
Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part II: complete WSTS. Log. Methods Comput. Sci. 8(3) (2012)
Geeraerts, G., Raskin, J., Begin, L.V.: Expand, enlarge and check: new algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72(1), 180–203 (2006)
Geeraerts, G., Raskin, J.-F., Van Begin, L.: On the efficient computation of the coverability set for petri nets. Int. J. Found. Comput. Sci. 21(2), 135–165 (2010)
Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)
Kloos, J., Majumdar, R., Niksic, F., Piskac, R.: Incremental, inductive coverability. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 158–173. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_10
Li, Y., Deutsch, A., Vianu, V.: VERIFAS: a practical verifier for artifact systems. Proc. VLDB Endow. 11(3), 283–296 (2017)
Lüttge, K.: Zustandsgraphen von Petri-Netzen. Master’s thesis, Humboldt-Universität (1995)
Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Institut für Instrumentelle Mathematik, Bonn, Germany (1962)
Piipponen, A., Valmari, A.: Constructing minimal coverability sets. Fundam. Inf. 143(3–4), 393–414 (2016)
Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223–231 (1978)
Reynier, P.-A., Servais, F.: Minimal coverability set for Petri nets: Karp and Miller algorithm with pruning. Fundam. Inf. 122(1–2), 1–30 (2013)
Schmidt, K.: Model-checking with coverability graphs. Form. Methods Syst. Des. 15(3), 239–254 (1999)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Reynier, PA., Servais, F. (2019). On the Computation of the Minimal Coverability Set of Petri Nets. In: Filiot, E., Jungers, R., Potapov, I. (eds) Reachability Problems. RP 2019. Lecture Notes in Computer Science(), vol 11674. Springer, Cham. https://doi.org/10.1007/978-3-030-30806-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-30806-3_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30805-6
Online ISBN: 978-3-030-30806-3
eBook Packages: Computer ScienceComputer Science (R0)