{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T01:51:42Z","timestamp":1743040302741,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572456"},{"type":"electronic","value":"9783031572463"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T00:00:00Z","timestamp":1712188800000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Petri nets constitute a well-studied model to verify and study concurrent systems, among others, and computing the coverability set is one of the most fundamental problems about Petri nets. Using the proof assistant <jats:sc>Coq<\/jats:sc>, we certified the correctness and termination of the <jats:sc>MinCov<\/jats:sc> algorithm by Finkel, Haddad, and Khmelnitsky (FOSSACS 2020). This algorithm is the most recent algorithm in the literature that computes the minimal basis of the coverability set, a problem known to be prone to subtle bugs. Apart from the intrinsic interest of a computer-checked proof, our certification provides new insights on the <jats:sc>MinCov<\/jats:sc> algorithm. In particular, we introduce as an intermediate algorithm a small-step variant of <jats:sc>MinCov<\/jats:sc> of independent interest.<\/jats:p>","DOI":"10.1007\/978-3-031-57246-3_21","type":"book-chapter","created":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T14:03:43Z","timestamp":1712153023000},"page":"370-389","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A State-of-the-Art Karp-Miller Algorithm Certified in Coq"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-7324-8767","authenticated-orcid":false,"given":"Thibault","family":"Hilaire","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0094-4330","authenticated-orcid":false,"given":"David","family":"Ilcinkas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7214-9467","authenticated-orcid":false,"given":"J\u00e9r\u00f4me","family":"Leroux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,4]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","unstructured":"Angeli, D., Leenheer, P.D., Sontag, E.D.: Persistence results for chemical reaction networks with time-dependent kinetics and no global conservation laws. SIAM Journal on Applied Mathematics 71(1), 128\u2013146 (2011). https:\/\/doi.org\/10.1137\/090779401, http:\/\/www.jstor.org\/stable\/41111581","DOI":"10.1137\/090779401"},{"key":"21_CR2","doi-asserted-by":"publisher","unstructured":"Baldan, P., Cocco, N., Marin, A., Simeoni, M.: Petri nets for modelling metabolic pathways: A survey. Natural Computing 9, 955\u2013989 (12 2010). https:\/\/doi.org\/10.1007\/s11047-010-9180-6","DOI":"10.1007\/s11047-010-9180-6"},{"key":"21_CR3","doi-asserted-by":"publisher","unstructured":"Blondin, M., Haase, C., Offtermatt, P.: Directed Reachability for Infinite-State Systems. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12652, pp. 3\u201323. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_1","DOI":"10.1007\/978-3-030-72013-1_1"},{"key":"21_CR4","doi-asserted-by":"publisher","unstructured":"Bozzelli, L., Ganty, P.: Complexity Analysis of the Backward Coverability Algorithm for VASS. In: Delzanno, G., Potapov, I. (eds.) Reachability Problems - 5th International Workshop, RP 2011, Genoa, Italy, September 28-30, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06945, pp. 96\u2013109. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-24288-5_10","DOI":"10.1007\/978-3-642-24288-5_10"},{"key":"21_CR5","doi-asserted-by":"publisher","unstructured":"Czerwinski, W., Lasota, S., Lazic, R., Leroux, J., Mazowiecki, F.: The reachability problem for Petri nets is not elementary. In: Charikar, M., Cohen, E. (eds.) Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019. pp. 24\u201333. ACM (2019). https:\/\/doi.org\/10.1145\/3313276.3316369","DOI":"10.1145\/3313276.3316369"},{"key":"21_CR6","doi-asserted-by":"publisher","unstructured":"Czerwinski, W., Orlikowski, L.: Reachability in Vector Addition Systems is Ackermann-complete. In: 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022. pp. 1229\u20131240. IEEE (2021). https:\/\/doi.org\/10.1109\/FOCS52979.2021.00120","DOI":"10.1109\/FOCS52979.2021.00120"},{"key":"21_CR7","doi-asserted-by":"publisher","unstructured":"Dixon, A., Lazic, R.: KReach: A Tool for Reachability in Petri Nets. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12078, pp. 405\u2013412. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_22","DOI":"10.1007\/978-3-030-45190-5_22"},{"key":"21_CR8","doi-asserted-by":"publisher","unstructured":"Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and Primitive-Recursive Bounds with Dickson\u2019s Lemma. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada. pp. 269\u2013278. IEEE Computer Society (2011). https:\/\/doi.org\/10.1109\/LICS.2011.39","DOI":"10.1109\/LICS.2011.39"},{"key":"21_CR9","doi-asserted-by":"publisher","unstructured":"Finkel, A.: The Minimal Coverability Graph for Petri Nets. In: Rozenberg, G. (ed.) Advances in Petri Nets 1993, Papers from the 12th International Conference on Applications and Theory of Petri Nets, Gjern, Denmark, June 1991. Lecture Notes in Computer Science, vol.\u00a0674, pp. 210\u2013243. Springer (1991). https:\/\/doi.org\/10.1007\/3-540-56689-9_45","DOI":"10.1007\/3-540-56689-9_45"},{"key":"21_CR10","unstructured":"Finkel, A., Geeraerts, G., Raskin, J.F., Van\u00a0Begin, L.: A counter-example to the minimal coverability tree algorithm. Universit\u00e9 Libre de Bruxelles, Tech. Rep 535 (2005)"},{"key":"21_CR11","doi-asserted-by":"publisher","unstructured":"Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part I: completions. Math. Struct. Comput. Sci. 30(7), 752\u2013832 (2020). https:\/\/doi.org\/10.1017\/S0960129520000195","DOI":"10.1017\/S0960129520000195"},{"key":"21_CR12","doi-asserted-by":"publisher","unstructured":"Finkel, A., Haddad, S., Khmelnitsky, I.: Minimal Coverability Tree Construction Made Complete and Efficient. In: Goubault-Larrecq, J., K\u00f6nig, B. (eds.) Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12077, pp. 237\u2013256. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45231-5_13","DOI":"10.1007\/978-3-030-45231-5_13"},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Geeraerts, G., Raskin, J.F., Van\u00a0Begin, L.: On the Efficient Computation of the Minimal Coverability Set for Petri Nets. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) Automated Technology for Verification and Analysis. pp. 98\u2013113. Springer Berlin Heidelberg, Berlin, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75596-8_9","DOI":"10.1007\/978-3-540-75596-8_9"},{"key":"21_CR14","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A small scale reflection extension for the Coq system. Ph.D. thesis, Inria Saclay Ile de France (2016)"},{"key":"21_CR15","unstructured":"Hack, M.: Decidability Questions for Petri Nets. Outstanding Dissertations in the Computer Sciences, Garland Publishing, New York (1975)"},{"key":"21_CR16","unstructured":"Hilaire, T., Ilcinkas, D., Leroux, J.: Petri-net-in-coq (2024), https:\/\/archive.softwareheritage.org\/swh:1:rev:7b5523e30026266c471c73e911f0fda525c6f900; origin=https:\/\/gitub.u-bordeaux.fr\/thhilaire\/petri-net-in-coq.git"},{"key":"21_CR17","doi-asserted-by":"publisher","unstructured":"Jan\u010dar, P.: Decidability of a Temporal Logic Problem for Petri Nets. Theor. Comput. Sci. 74(1), 71\u201393 (1990). https:\/\/doi.org\/10.1016\/0304-3975(90)90006-4","DOI":"10.1016\/0304-3975(90)90006-4"},{"key":"21_CR18","doi-asserted-by":"publisher","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Efficient Coverability Analysis by Proof Minimization. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012 - Concurrency Theory - 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07454, pp. 500\u2013515. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_35","DOI":"10.1007\/978-3-642-32940-1_35"},{"key":"21_CR19","doi-asserted-by":"publisher","unstructured":"Karp, R.M., Miller, R.E.: Parallel Program Schemata. J. Comput. Syst. Sci. 3(2), 147\u2013195 (1969). https:\/\/doi.org\/10.1016\/S0022-0000(69)80011-5","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"21_CR20","doi-asserted-by":"publisher","unstructured":"Lasota, S.: Improved Ackermannian Lower Bound for the Petri Nets Reachability Problem. In: Berenbrink, P., Monmege, B. (eds.) 39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022, March 15-18, 2022, Marseille, France (Virtual Conference). LIPIcs, vol.\u00a0219, pp. 46:1\u201346:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2022.46","DOI":"10.4230\/LIPIcs.STACS.2022.46"},{"key":"21_CR21","doi-asserted-by":"publisher","unstructured":"Lazic, R., Schmitz, S.: The ideal view on Rackoff\u2019s coverability technique. Inf. Comput. 277, 104582 (2021). https:\/\/doi.org\/10.1016\/j.ic.2020.104582","DOI":"10.1016\/j.ic.2020.104582"},{"key":"21_CR22","doi-asserted-by":"publisher","unstructured":"Leroux, J.: Vector addition system reachability problem: a short self-contained proof. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011. pp. 307\u2013316. ACM (2011). https:\/\/doi.org\/10.1145\/1926385.1926421","DOI":"10.1145\/1926385.1926421"},{"key":"21_CR23","doi-asserted-by":"publisher","unstructured":"Leroux, J.: The Reachability Problem for Petri Nets is Not Primitive Recursive. In: 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022. pp. 1241\u20131252. IEEE (2021). https:\/\/doi.org\/10.1109\/FOCS52979.2021.00121","DOI":"10.1109\/FOCS52979.2021.00121"},{"key":"21_CR24","doi-asserted-by":"publisher","unstructured":"Leroux, J., Schmitz, S.: Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. In: 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. pp. 1\u201313. IEEE (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785796","DOI":"10.1109\/LICS.2019.8785796"},{"key":"21_CR25","doi-asserted-by":"publisher","unstructured":"Mayr, E.W., Meyer, A.R.: The Complexity of the Finite Containment Problem for Petri Nets. J. ACM 28(3), 561\u2013576 (1981). https:\/\/doi.org\/10.1145\/322261.322271","DOI":"10.1145\/322261.322271"},{"key":"21_CR26","doi-asserted-by":"publisher","unstructured":"Peleg, M., Rubin, D., Altman, R.B.: Using Petri Net Tools to Study Properties and Dynamics of Biological Systems. Journal of the American Medical Informatics Association 12(2), 181\u2013199 (03 2005). https:\/\/doi.org\/10.1197\/jamia.M1637","DOI":"10.1197\/jamia.M1637"},{"key":"21_CR27","doi-asserted-by":"publisher","unstructured":"Piipponen, A., Valmari, A.: Constructing Minimal Coverability Sets. Fundam. Informaticae 143(3-4), 393\u2013414 (2016). https:\/\/doi.org\/10.3233\/FI-2016-1319","DOI":"10.3233\/FI-2016-1319"},{"key":"21_CR28","doi-asserted-by":"publisher","unstructured":"Rackoff, C.: The Covering and Boundedness Problems for Vector Addition Systems. Theor. Comput. Sci. 6, 223\u2013231 (1978). https:\/\/doi.org\/10.1016\/0304-3975(78)90036-1","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"21_CR29","doi-asserted-by":"publisher","unstructured":"Reynier, P.A., Servais, F.: Minimal coverability set for petri nets: Karp and miller algorithm with pruning. In: International Conference on Application and Theory of Petri Nets and Concurrency. pp. 69\u201388. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-21834-7_5","DOI":"10.1007\/978-3-642-21834-7_5"},{"key":"21_CR30","doi-asserted-by":"publisher","unstructured":"Reynier, P., Servais, F.: On the Computation of the Minimal Coverability Set of Petri Nets. In: Filiot, E., Jungers, R.M., Potapov, I. (eds.) Reachability Problems - 13th International Conference, RP 2019, Brussels, Belgium, September 11-13, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11674, pp. 164\u2013177. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-30806-3_13","DOI":"10.1007\/978-3-030-30806-3_13"},{"key":"21_CR31","doi-asserted-by":"publisher","unstructured":"Schmitz, S.: The complexity of reachability in vector addition systems. ACM SIGLOG News 3(1), 4\u201321 (2016). https:\/\/doi.org\/10.1145\/2893582.2893585","DOI":"10.1145\/2893582.2893585"},{"key":"21_CR32","doi-asserted-by":"publisher","unstructured":"Vytiniotis, D., Coquand, T., Wahlstedt, D.: Stop When You Are Almost-Full - Adventures in Constructive Termination. In: Beringer, L., Felty, A.P. (eds.) Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07406, pp. 250\u2013265. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_17","DOI":"10.1007\/978-3-642-32347-8_17"},{"key":"21_CR33","doi-asserted-by":"publisher","unstructured":"Yamamoto, M., Sekine, S., Matsumoto, S.: Formalization of Karp-Miller tree construction on petri nets. In: Bertot, Y., Vafeiadis, V. (eds.) Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. pp. 66\u201378. ACM (2017). https:\/\/doi.org\/10.1145\/3018610.3018626","DOI":"10.1145\/3018610.3018626"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57246-3_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T14:09:18Z","timestamp":1712153358000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57246-3_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572456","9783031572463"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57246-3_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"4 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}