{"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":1790791334356,"version":"4.1.0"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720124","type":"print"},{"value":"9783030720131","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computationally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph exploration algorithms such as <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {A}^{*}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:msup>\n                      <mml:mrow>\n                        <mml:mi>A<\/mml:mi>\n                      <\/mml:mrow>\n                      <mml:mrow>\n                        <mml:mrow\/>\n                        <mml:mo>\u2217<\/mml:mo>\n                      <\/mml:mrow>\n                    <\/mml:msup>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and greedy best-first search. We provide and evaluate a prototype implementation of our approach that outperforms existing state-of-the-art tools, sometimes by orders of magnitude, and which is also competitive with domain-specific tools on benchmarks coming from program synthesis and concurrent program analysis.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_1","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"3-23","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Directed Reachability for Infinite-State Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2914-2734","authenticated-orcid":false,"given":"Michael","family":"Blondin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5452-936X","authenticated-orcid":false,"given":"Christoph","family":"Haase","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8477-2849","authenticated-orcid":false,"given":"Philip","family":"Offtermatt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: Proc. $$\\text{11}^\\text{th }$$ Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 313\u2013321. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561359","DOI":"10.1109\/LICS.1996.561359"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Angeli, D., De Leenheer, P., Sontag, E.D.: A Petri net approach to the study of persistence in chemical reaction networks. Mathematical Biosciences 210(2), 598\u2013618 (2007). https:\/\/doi.org\/10.1016\/j.mbs.2007.07.003","DOI":"10.1016\/j.mbs.2007.07.003"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Araki, T., Kasami, T.: Some decision problems related to the reachability problem for Petri nets. Theoretical Computer Science 3(1), 85\u2013104 (1976). https:\/\/doi.org\/10.1016\/0304-3975(76)90067-0","DOI":"10.1016\/0304-3975(76)90067-0"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Athanasiou, K., Liu, P., Wahl, T.: Unbounded-thread program verification using thread-state equations. In: Proc. $${{8}^{\\rm th}}$$ International Joint Conference on Automated Reasoning (IJCAR). pp. 516\u2013531. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_35","DOI":"10.1007\/978-3-319-40229-1_35"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Bansal, K., Koskinen, E., Wies, T., Zufferey, D.: Structural counter abstraction. In: Proc. $${{19}^{{\\rm th}}}$$ International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 62\u201377. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_5","DOI":"10.1007\/978-3-642-36742-7_5"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Barth, A., Mitchell, J.C., Datta, A., Sundaram, S.: Privacy and utility in business processes. In: Proc. $${{20}^{\\rm th}}$$ IEEE Computer Security Foundations Symposium (CSF). pp. 279\u2013294. IEEE Computer Society (2007). https:\/\/doi.org\/10.1109\/CSF.2007.26","DOI":"10.1109\/CSF.2007.26"},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N., Phan, A., Fleckenstein, L.: $$\\nu $$Z - an optimizing SMT solver. In: Proc. $${{21}^{\\rm th}}$$ International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 194\u2013199. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_14","DOI":"10.1007\/978-3-662-46681-0_14"},{"key":"1_CR8","doi-asserted-by":"publisher","unstructured":"Blondin, M., Finkel, A., Haase, C., Haddad, S.: The logical view on continuous Petri nets. ACM Transactions on Computational Logic (TOCL) 18(3), 24:1\u201324:28 (2017). https:\/\/doi.org\/10.1145\/3105908","DOI":"10.1145\/3105908"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Blondin, M., Haase, C., Mazowiecki, F.: Affine extensions of integer vector addition systems with states. In: Proc. $${{29}^{\\rm th}}$$ International Conference on Concurrency Theory (CONCUR). pp. 14:1\u201314:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.14","DOI":"10.4230\/LIPIcs.CONCUR.2018.14"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Blondin, M., Haase, C., Offtermatt, P.: Fastforward: A tool for reachability in Petri nets with infinite state spaces. Artifact for the TACAS21 contribution \u201cDirected Reachability for Infinite-State Systems\u201d (2021). https:\/\/doi.org\/10.6084\/m9.figshare.13573592","DOI":"10.6084\/m9.figshare.13573592"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Chaouiya, C.: Petri net modelling of biological networks. Briefings in Bioinformatics 8(4), 210\u2013219 (2007). https:\/\/doi.org\/10.1093\/bib\/bbm029","DOI":"10.1093\/bib\/bbm029"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Chistikov, D., Haase, C., Halfon, S.: Context-free commutative grammars with integer counters and resets. Theoretical Computer Science 735, 147\u2013161 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2016.06.017","DOI":"10.1016\/j.tcs.2016.06.017"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Czerwi\u0144ski, W., Lasota, S., Lazi\u0107, R., Leroux, J., Mazowiecki, F.: The reachability problem for Petri nets is not elementary. In: Proc. $${{51}^{\\rm st}}$$ Annual ACM SIGACT Symposium on Theory of Computing (STOC). pp. 24\u201333. ACM (2019). https:\/\/doi.org\/10.1145\/3313276.3316369","DOI":"10.1145\/3313276.3316369"},{"key":"1_CR14","unstructured":"David, R., Alla, H.: Continuous Petri nets. In: Proc. $${{8}^{\\rm th}}$$ European Workshop on Application and Theory of Petri nets. vol.\u00a0340, pp. 275\u2013294 (1987)"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"David, R., Alla, H.: Discrete, Continuous, and Hybrid Petri nets. Springer, $${{2}^{\\rm nd}}$$ edn. (2010)","DOI":"10.1007\/978-3-642-10669-9"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Delzanno, G., Raskin, J., Van Begin, L.: Towards the automated verification of multithreaded Java programs. In: Proc. $${{8}^{\\rm th}}$$ International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 173\u2013187. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_13","DOI":"10.1007\/3-540-46002-0_13"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Dixon, A., Lazi\u0107, R.: Kreach: A tool for reachability in Petri nets. In: Proc. $${{26}^{\\rm th}}$$ International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 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":"1_CR18","doi-asserted-by":"publisher","unstructured":"D\u2019Osualdo, E., Kochems, J., Ong, C.L.: Automatic verification of erlang-style concurrency. In: Proc. $${{20}^{\\rm th}}$$ International Symposium on Static Analysis (SAS). pp. 454\u2013476. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_24","DOI":"10.1007\/978-3-642-38856-9_24"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Proc. $${{25}^{\\rm th}}$$ International Colloquium on Automata, Languages and Programming (ICALP). pp. 103\u2013115. Springer (1998). https:\/\/doi.org\/10.1007\/BFb0055044","DOI":"10.1007\/BFb0055044"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Edelkamp, S., Schuppan, V., Bosnacki, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on directed model checking. In: Proc. $${{5}^{\\rm th}}$$ International Workshop on Model Checking and Artificial Intelligence (MoChArt). pp. 65\u201389. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-642-00431-5_5","DOI":"10.1007\/978-3-642-00431-5_5"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Esparza, J.: Decidability and complexity of Petri net problems \u2014 An introduction, pp. 374\u2013428. Springer (1998). https:\/\/doi.org\/10.1007\/3-540-65306-6_20","DOI":"10.1007\/3-540-65306-6_20"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Verification of population protocols. Acta Informatica 54(2), 191\u2013215 (2017). https:\/\/doi.org\/10.1007\/s00236-016-0272-3","DOI":"10.1007\/s00236-016-0272-3"},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P.J., Nik\u0161i\u0107, F.: An SMT-based approach to coverability analysis. In: Proc. $${{26}^{\\rm th}}$$ International Conference on Computer Aided Verification (CAV). pp. 603\u2013619. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_40","DOI":"10.1007\/978-3-319-08867-9_40"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Feng, Y., Martins, R., Wang, Y., Dillig, I., Reps, T.W.: Component-based synthesis for complex APIs. In: Proc. $${{44}^{\\rm th}}$$ ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). pp. 599\u2013612. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009851","DOI":"10.1145\/3009837.3009851"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Fraca, E., Haddad, S.: Complexity analysis of continuous Petri nets. Fundamenta Informaticae 137(1), 1\u201328 (2015). https:\/\/doi.org\/10.3233\/FI-2015-1168","DOI":"10.3233\/FI-2015-1168"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Galenson, J.: Dynamic and Interactive Synthesis of Code Snippets. Ph.D. thesis, University of California (2014)","DOI":"10.1145\/2568225.2568250"},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"Galenson, J., Reames, P., Bod\u00edk, R., Hartmann, B., Sen, K.: Codehint: dynamic and interactive synthesis of code snippets. In: Proc. $${{36}^{\\rm th}}$$ International Conference on Software Engineering (ICSE). pp. 653\u2013663. ACM (2014). https:\/\/doi.org\/10.1145\/2568225.2568250","DOI":"10.1145\/2568225.2568250"},{"key":"1_CR28","unstructured":"Ganty, P.: Algorithmes et structures de donn\u00e9es efficaces pour la manipulation de contraintes sur les intervalles. Master\u2019s thesis, Universit\u00e9 Libre de Bruxelles (2002), (In French)"},{"key":"1_CR29","doi-asserted-by":"publisher","unstructured":"Geffroy, T., Leroux, J., Sutre, G.: Occam\u2019s razor applied to the Petri net coverability problem. Theoretical Computer Science 750, 38\u201352 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2018.04.014","DOI":"10.1016\/j.tcs.2018.04.014"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. Journal of the ACM 39(3), 675\u2013735 (1992). https:\/\/doi.org\/10.1145\/146637.146681","DOI":"10.1145\/146637.146681"},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"Gupta, U., Shah, P., Akshay, S., Hofman, P.: Continuous reachability for unordered data Petri nets is in PTime. In: Proc. $${{22}^{\\rm nd}}$$ International Conference on Foundations of Software Science and Computation Structures (FoSSaCS). pp. 260\u2013276. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17127-8_15","DOI":"10.1007\/978-3-030-17127-8_15"},{"key":"1_CR32","unstructured":"Gurobi\u00a0Optimization, L.: Gurobi optimizer reference manual (2020), http:\/\/www.gurobi.com"},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"Heiner, M., Gilbert, D.R., Donaldson, R.: Petri nets for systems and synthetic biology. In: Formal Methods for Computational Systems Biology. pp. 215\u2013264. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-68894-5_7","DOI":"10.1007\/978-3-540-68894-5_7"},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Hofman, P., Leroux, J., Totzke, P.: Linear combinations of unordered data vectors. In: Proc. $${{32}^{\\rm nd}}$$ Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). pp. 1\u201311. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005065","DOI":"10.1109\/LICS.2017.8005065"},{"key":"1_CR35","unstructured":"Jan\u00e1k, J.: Issue Tracking Systems. Master\u2019s thesis, Masaryk University (2009)"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Jeng, M.D., Chen, S.C.: A heuristic search approach using approximate solutions to Petri net state equations for scheduling flexible manufacturing systems. International Journal of Flexible Manufacturing Systems 10(2), 139\u2013162 (1998). https:\/\/doi.org\/10.1023\/A:1008097430956","DOI":"10.1023\/A:1008097430956"},{"key":"1_CR37","unstructured":"Jensen, K.: Coloured Petri nets: basic concepts, analysis methods and practical use, vol.\u00a01. Springer Science & Business Media (2013)"},{"key":"1_CR38","doi-asserted-by":"publisher","unstructured":"Jones, N.D., Landweber, L.H., Lien, Y.E.: Complexity of some problems in Petri nets. Theoretical Computer Science 4(3), 277\u2013299 (1977). https:\/\/doi.org\/10.1016\/0304-3975(77)90014-7","DOI":"10.1016\/0304-3975(77)90014-7"},{"key":"1_CR39","doi-asserted-by":"publisher","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: A widening approach to multithreaded program verification. ACM Transactions on Programming Languages and Systems (TOPLAS) 36(4), 14:1\u201314:29 (2014). https:\/\/doi.org\/10.1145\/2629608","DOI":"10.1145\/2629608"},{"key":"1_CR40","doi-asserted-by":"publisher","unstructured":"Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: Proc. $${{14}^{\\rm th}}$$ Symposium on Theory of Computing (STOC). pp. 267\u2013281. ACM (1982). https:\/\/doi.org\/10.1145\/800070.802201","DOI":"10.1145\/800070.802201"},{"key":"1_CR41","doi-asserted-by":"publisher","unstructured":"Lambert, J.: A structure to decide reachability in Petri nets. Theoretical Computer Science 99(1), 79\u2013104 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90173-D","DOI":"10.1016\/0304-3975(92)90173-D"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Lee, D.Y., DiCesare, F.: Scheduling flexible manufacturing systems using Petri nets and heuristic search. IEEE Transactions on robotics and automation 10(2), 123\u2013132 (1994). https:\/\/doi.org\/10.1109\/70.282537","DOI":"10.1109\/70.282537"},{"key":"1_CR43","unstructured":"Leroux, J.: Vector addition systems reachability problem (A simpler solution). In: Turing-100 - The Alan Turing Centenary. pp. 214\u2013228. EasyChair (2012)."},{"key":"1_CR44","doi-asserted-by":"publisher","unstructured":"Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: Proc. $${{30}^{\\rm th}}$$ Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). pp. 56\u201367. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/LICS.2015.16","DOI":"10.1109\/LICS.2015.16"},{"key":"1_CR45","unstructured":"Lipton, R.J.: The reachability problem requires exponential space. Tech. rep., Yale University (1976)"},{"key":"1_CR46","doi-asserted-by":"publisher","unstructured":"Liu, B., Dong, W., Zhang, Y.: Accelerating API-based program synthesis via API usage pattern mining. IEEE Access 7, 159162\u2013159176 (2019). https:\/\/doi.org\/10.1109\/ACCESS.2019.2950232","DOI":"10.1109\/ACCESS.2019.2950232"},{"key":"1_CR47","doi-asserted-by":"publisher","unstructured":"Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: Proc. $${{13}^{\\rm th}}$$ Symposium on Theory of Computing (STOC). pp. 238\u2013246. ACM (1981). https:\/\/doi.org\/10.1145\/800076.802477","DOI":"10.1145\/800076.802477"},{"key":"1_CR48","doi-asserted-by":"publisher","unstructured":"Mej\u00eda, G., Odrey, N.G.: An approach using Petri nets and improved heuristic search for manufacturing system scheduling. Journal of Manufacturing Systems 24(2), 79\u201392 (2005). https:\/\/doi.org\/10.1016\/S0278-6125(05)80009-3","DOI":"10.1016\/S0278-6125(05)80009-3"},{"key":"1_CR49","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proc. $${{14}^{\\rm th}}$$ International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24, tool available at https:\/\/github.com\/Z3Prover\/z3.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"1_CR50","doi-asserted-by":"publisher","unstructured":"Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541\u2013580 (1989). https:\/\/doi.org\/10.1109\/5.24143","DOI":"10.1109\/5.24143"},{"key":"1_CR51","doi-asserted-by":"publisher","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6, 223\u2013231 (1978). https:\/\/doi.org\/10.1016\/0304-3975(78)90036-1","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"1_CR52","unstructured":"Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach. Prentice Hall Press, $${{3}^{\\rm rd}}$$ edn. (2009)"},{"key":"1_CR53","doi-asserted-by":"publisher","unstructured":"Schmidt, K.: LoLA: A low level analyser. In: Proc. International Conference on Application and Theory of Petri Nets (ICATPN). pp. 465\u2013474. Springer (2000). https:\/\/doi.org\/10.1007\/3-540-44988-4_27","DOI":"10.1007\/3-540-44988-4_27"},{"key":"1_CR54","doi-asserted-by":"publisher","unstructured":"Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: Proc. $${{31}^{\\rm st}}$$ International Conference on Computer Aided Verification (CAV). pp. 97\u2013115. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_7","DOI":"10.1007\/978-3-030-25543-5_7"},{"key":"1_CR55","unstructured":"Strazny, T.: An algorithmic framework for checking coverability in well-structured transition systems. Ph.D. thesis, Universit\u00e4t Oldenburg (2014), http:\/\/csd.informatik.uni-oldenburg.de\/~skript\/pub\/diss\/strazny-phdthesis-roterbericht.pdf"},{"key":"1_CR56","doi-asserted-by":"publisher","unstructured":"Uma, G., Prasad, B.: Reachability trees for Petri nets: a heuristic approach. Knowledge-Based Systems 6(3), 174 \u2013 177 (1993). https:\/\/doi.org\/10.1016\/0950-7051(93)90042-R","DOI":"10.1016\/0950-7051(93)90042-R"},{"key":"1_CR57","doi-asserted-by":"publisher","unstructured":"van der Aalst, W.: The application of Petri nets to workflow management. Journal of Circuits, Systems, and Computers 8(1), 21\u201366 (1998). https:\/\/doi.org\/10.1142\/S0218126698000043","DOI":"10.1142\/S0218126698000043"},{"key":"1_CR58","doi-asserted-by":"publisher","unstructured":"Watel, D., Weisser, M., Barth, D.: Parameterized complexity and approximability of coverability problems in weighted Petri nets. In: Proc. $${{38}^{\\rm th}}$$ International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS). pp. 330\u2013349. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-57861-3_19","DOI":"10.1007\/978-3-319-57861-3_19"},{"key":"1_CR59","doi-asserted-by":"publisher","unstructured":"Wynn, M.T., van\u00a0der Aalst, W.M.P., ter Hofstede, A.H.M., Edmond, D.: Synchronization and cancelation in workflows based on reset nets. International Journal of Cooperative Information Systems 18(1), 63\u2013114 (2009). https:\/\/doi.org\/10.1142\/S0218843009002002","DOI":"10.1142\/S0218843009002002"},{"key":"1_CR60","doi-asserted-by":"publisher","unstructured":"Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Proc. $${{35}^{\\rm th}}$$ Conference on Design Automation (DAC). pp. 599\u2013604. ACM (1998). https:\/\/doi.org\/10.1145\/277044.277201","DOI":"10.1145\/277044.277201"},{"key":"1_CR61","doi-asserted-by":"publisher","unstructured":"Zuck, L.D., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Computer Languages, Systems & Structures 30(3-4), 139\u2013169 (2004). https:\/\/doi.org\/10.1016\/j.cl.2004.02.006","DOI":"10.1016\/j.cl.2004.02.006"}],"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-72013-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:09:48Z","timestamp":1616436588000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/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":"141","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":"41","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":"21","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":"29% - 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 changed to an online format due to the COVID-19 pandemic","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)"}}]}}