{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T18:02:14Z","timestamp":1790791334944,"version":"4.1.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030451899","type":"print"},{"value":"9783030451905","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]]},"DOI":"10.1007\/978-3-030-45190-5_22","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T09:03:02Z","timestamp":1587114182000},"page":"405-412","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["KReach: A Tool for Reachability in Petri Nets"],"prefix":"10.1007","author":[{"given":"Alex","family":"Dixon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ranko","family":"Lazi\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"22_CR1","unstructured":"Control.Concurrent - Haskell Package Database. \nhttp:\/\/hackage.haskell.org\/package\/base-4.12.0.0\/docs\/Control-Concurrent.html"},{"key":"22_CR2","unstructured":"Mist - a safety checker for Petri nets (and monotonic extensions). \nhttps:\/\/github.com\/pierreganty\/mist"},{"key":"22_CR3","doi-asserted-by":"publisher","unstructured":"Angeli, D., De Leenheer, P., 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). \nhttps:\/\/doi.org\/10.1137\/090779401","DOI":"10.1137\/090779401"},{"key":"22_CR4","doi-asserted-by":"publisher","unstructured":"Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously. In: TACAS. LNCS, vol. 9636, pp. 480\u2013496. Springer (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49674-9_28","DOI":"10.1007\/978-3-662-49674-9_28"},{"key":"22_CR5","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Emmi, M.: Analysis of recursively parallel programs. ACM Trans. Program. Lang. Syst. 35(3) (Nov 2013). \nhttps:\/\/doi.org\/10.1145\/2518188","DOI":"10.1145\/2518188"},{"key":"22_CR6","doi-asserted-by":"publisher","unstructured":"Burns, F., Koelmans, A., Yakovlev, A.: WCET analysis of Superscalar Processors using Simulation with coloured Petri nets. Real-Time Systems 18, 275\u2013288 (2000). \nhttps:\/\/doi.org\/10.1023\/A:1008101416758","DOI":"10.1023\/A:1008101416758"},{"key":"22_CR7","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: STOC. pp. 24\u201333. ACM (2019). \nhttps:\/\/doi.org\/10.1145\/3313276.3316369","DOI":"10.1145\/3313276.3316369"},{"key":"22_CR8","doi-asserted-by":"publisher","unstructured":"Demri, S., Figueira, D., Praveen, M.: Reasoning about data repetitions with counter systems. Logical Methods in Computer Science 12(3) (2016). \nhttps:\/\/doi.org\/10.2168\/LMCS-12(3:1)2016","DOI":"10.2168\/LMCS-12(3:1)2016"},{"key":"22_CR9","doi-asserted-by":"publisher","unstructured":"Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Verification of population protocols. Acta Inf. 54(2), 191\u2013215 (2017). \nhttps:\/\/doi.org\/10.1007\/s00236-016-0272-3","DOI":"10.1007\/s00236-016-0272-3"},{"key":"22_CR10","unstructured":"Finkel, A., Haddad, S., Khmelnitsky, I.: Minimal coverability tree construction made complete and efficient. In: FoSSaCS (2020), \nhttps:\/\/hal.inria.fr\/hal-02479879"},{"key":"22_CR11","doi-asserted-by":"publisher","unstructured":"Geffroy, T., Leroux, J., Sutre, G.: Occam\u2019s razor applied to the petri net coverability problem. Theor. Comput. Sci. 750, 38\u201352 (2018). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2018.04.014","DOI":"10.1016\/j.tcs.2018.04.014"},{"key":"22_CR12","doi-asserted-by":"publisher","unstructured":"Greibach, S.A.: Remarks on blind and partially blind one-way multicounter machines. Theor. Comput. Sci. 7, 311\u2013324 (1978). \nhttps:\/\/doi.org\/10.1016\/0304-3975(78)90020-8","DOI":"10.1016\/0304-3975(78)90020-8"},{"key":"22_CR13","doi-asserted-by":"publisher","unstructured":"Hack, M.: The recursive equivalence of the reachability problem and the liveness problem for petri nets and vector addition systems. In: 15th Annual Symposium on Switching and Automata Theory (swat 1974). pp. 156\u2013164 (Oct 1974). \nhttps:\/\/doi.org\/10.1109\/SWAT.1974.28","DOI":"10.1109\/SWAT.1974.28"},{"key":"22_CR14","doi-asserted-by":"publisher","unstructured":"Hopcroft, J.E., Pansiot, J.: On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci. 8, 135\u2013159 (1979). \nhttps:\/\/doi.org\/10.1016\/0304-3975(79)90041-0","DOI":"10.1016\/0304-3975(79)90041-0"},{"key":"22_CR15","doi-asserted-by":"publisher","unstructured":"Kanovich, M.I.: Petri nets, Horn programs, linear logic and vector games. Ann. Pure Appl. Logic 75(1\u20132), 107\u2013135 (1995). \nhttps:\/\/doi.org\/10.1016\/0168-0072(94)00060-G","DOI":"10.1016\/0168-0072(94)00060-G"},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147\u2013195 (1969). \nhttps:\/\/doi.org\/10.1016\/S0022-0000(69)80011-5","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"22_CR17","doi-asserted-by":"publisher","unstructured":"Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: STOC. pp. 267\u2013281. ACM (1982). \nhttps:\/\/doi.org\/10.1145\/800070.802201","DOI":"10.1145\/800070.802201"},{"key":"22_CR18","doi-asserted-by":"publisher","unstructured":"Lambert, J.: A structure to decide reachability in Petri nets. Theor. Comput. Sci. 99(1), 79\u2013104 (1992). \nhttps:\/\/doi.org\/10.1016\/0304-3975(92)90173-D","DOI":"10.1016\/0304-3975(92)90173-D"},{"key":"22_CR19","unstructured":"Lasota, S.: VASS reachability in three steps. CoRR abs\/1812.11966 (2018), \nhttp:\/\/arxiv.org\/abs\/1812.11966"},{"key":"22_CR20","doi-asserted-by":"publisher","unstructured":"Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. Logical Methods in Computer Science 6(3) (2010). \nhttps:\/\/doi.org\/10.2168\/LMCS-6(3:22)2010","DOI":"10.2168\/LMCS-6(3:22)2010"},{"key":"22_CR21","doi-asserted-by":"publisher","unstructured":"Leroux, J., Schmitz, S.: Reachability in vector addition systems is primitive-recursive in fixed dimension. In: LICS. pp. 1\u201313. IEEE (2019). \nhttps:\/\/doi.org\/10.1109\/LICS.2019.8785796","DOI":"10.1109\/LICS.2019.8785796"},{"key":"22_CR22","doi-asserted-by":"publisher","unstructured":"Li, Y., Deutsch, A., Vianu, V.: VERIFAS: A practical verifier for artifact systems. PVLDB 11(3), 283\u2013296 (2017). \nhttps:\/\/doi.org\/10.14778\/3157794.3157798","DOI":"10.14778\/3157794.3157798"},{"key":"22_CR23","unstructured":"Lipton, R.J.: The reachability problem requires exponential space. Tech. Rep. 62, Yale University (1976), \nhttp:\/\/cpsc.yale.edu\/sites\/default\/files\/files\/tr63.pdf"},{"key":"22_CR24","doi-asserted-by":"publisher","unstructured":"Mayr, E.W.: An algorithm for the general petri net reachability problem. SIAM J. Comput. 13(3), 441\u2013460 (1984). \nhttps:\/\/doi.org\/10.1137\/0213029","DOI":"10.1137\/0213029"},{"key":"22_CR25","doi-asserted-by":"publisher","unstructured":"Meyer, R.: A theory of structural stationarity in the pi-calculus. Acta Inf. 46(2), 87\u2013137 (2009). \nhttps:\/\/doi.org\/10.1007\/s00236-009-0091-x","DOI":"10.1007\/s00236-009-0091-x"},{"key":"22_CR26","unstructured":"Petri, C.A.: Kommunikation mit Automaten. \nhttp:\/\/edoc.sub.uni-hamburg.de\/informatik\/volltexte\/2011\/160\/\n\n (1962), PhD thesis, Universit\u00e4t Hamburg"},{"key":"22_CR27","doi-asserted-by":"publisher","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223\u2013231 (1978). \nhttps:\/\/doi.org\/10.1016\/0304-3975(78)90036-1","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"22_CR28","unstructured":"Reutenauer, C.: The mathematics of Petri nets. Prentice Hall (1990), translated by Ian Craig"},{"key":"22_CR29","unstructured":"Reutenauer, C.: Aspects Math\u00e9matiques des R\u00e9seaux de Petri. Masson (1989)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45190-5_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,20]],"date-time":"2020-08-20T13:14:31Z","timestamp":1597929271000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45190-5_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030451899","9783030451905"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45190-5_22","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":"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":"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":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","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":"155","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":"40","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":"8","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":"26% - 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":"14","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)"}}]}}