{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T15:30:46Z","timestamp":1781019046745,"version":"3.54.1"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030452308","type":"print"},{"value":"9783030452315","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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  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.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_13","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"237-256","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Minimal Coverability Tree Construction Made Complete and Efficient"],"prefix":"10.1007","author":[{"given":"Alain","family":"Finkel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Serge","family":"Haddad","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Igor","family":"Khmelnitsky","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Blockelet, M., Schmitz, S.: Model checking coverability graphs of vector addition systems. In: Proceedings of MFCS 2011. LNCS, vol.\u00a06907, pp. 108\u2013119 (2011)","DOI":"10.1007\/978-3-642-22993-0_13"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously. In: Proceedings of TACAS 2016. LNCS, vol.\u00a09636, pp. 480\u2013496. Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_28"},{"key":"13_CR3","unstructured":"Blondin, M., Finkel, A., McKenzie, P.: Well behaved transition systems. Logical Methods in Computer Science 13(3), 1\u201319 (2017)"},{"key":"13_CR4","unstructured":"Demri, S.: On selective unboundedness of\u00a0VASS. J.\u00a0Comput. Syst. Sci. 79(5), 689\u2013713 (2013)"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Finkel, A.: Reduction and covering of infinite reachability trees. Information and Computation 89(2), 144\u2013179 (1990)","DOI":"10.1016\/0890-5401(90)90009-7"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Finkel, A.: The minimal coverability graph for Petri nets. In: Advances in Petri Nets. LNCS, vol.\u00a0674, pp. 210\u2013243 (1993)","DOI":"10.1007\/3-540-56689-9_45"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Finkel, A., Goubault-Larrecq, J.: Forward analysis for\u00a0WSTS, part\u00a0II: Complete WSTS. Logical Methods in Computer Science 8(4), 1\u201335 (2012)","DOI":"10.2168\/LMCS-8(3:28)2012"},{"key":"13_CR8","unstructured":"Finkel, A., Geeraerts, G., Raskin, J.F., Van\u00a0Begin, L.: A counter-example to the minimal coverability tree algorithm. Tech. rep., Universit\u00e9 Libre de Bruxelles, Belgium (2005), http:\/\/www.lsv.fr\/Publis\/PAPERS\/PDF\/FGRV-ulb05.pdf"},{"key":"13_CR9","unstructured":"Finkel, A., Haddad, S., Khmelnitsky, I.: Minimal coverability tree construction made complete and efficient (2020), https:\/\/hal.inria.fr\/hal-02479879"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"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\u2013165 (2010)","DOI":"10.1142\/S0129054110007180"},{"key":"13_CR11","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J.\u00a0Comput. Syst. Sci. 3(2), 147\u2013195 (1969)"},{"key":"13_CR12","unstructured":"Leroux, J.: Distance between mutually reachable Petri net configurations (Jun 2019), https:\/\/hal.archives-ouvertes.fr\/hal-02156549, preprint"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Piipponen, A., Valmari, A.: Constructing minimal coverability sets. Fundamenta Informaticae 143(3\u20134), 393\u2013414 (2016)","DOI":"10.3233\/FI-2016-1319"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Reynier, P.A., Servais, F.: Minimal coverability set for Petri nets: Karp and Miller algorithm with pruning. Fundamenta Informaticae 122(1\u20132), 1\u201330 (2013)","DOI":"10.3233\/FI-2013-781"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"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\u2013177 (2019)","DOI":"10.1007\/978-3-030-30806-3_13"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Valmari, A., Hansen, H.: Old and new algorithms for minimal coverability sets. Fundamenta Informaticae 131(1), 1\u201325 (2014)","DOI":"10.3233\/FI-2014-1002"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,7]],"date-time":"2021-01-07T13:31:44Z","timestamp":1610026304000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"98","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":"31","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":"0","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":"32% - 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":"12","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)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}