{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T20:12:48Z","timestamp":1770754368405,"version":"3.50.0"},"publisher-location":"Cham","reference-count":89,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031676949","type":"print"},{"value":"9783031676956","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,1]],"date-time":"2024-11-01T00:00:00Z","timestamp":1730419200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-67695-6_3","type":"book-chapter","created":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T14:03:04Z","timestamp":1730383384000},"page":"52-89","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Behind the\u00a0Scene of\u00a0the\u00a0Model Checking Contest, Analysis of\u00a0Results from\u00a02018 to\u00a02023"],"prefix":"10.1007","author":[{"given":"Nicolas","family":"Amat","sequence":"first","affiliation":[]},{"given":"Elvio","family":"Amparore","sequence":"additional","affiliation":[]},{"given":"Bernard","family":"Berthomieu","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Bouvier","sequence":"additional","affiliation":[]},{"given":"Silvano Dal","family":"Zilio","sequence":"additional","affiliation":[]},{"given":"Francis","family":"Hulin-Hubard","sequence":"additional","affiliation":[]},{"given":"Peter G.","family":"Jensen","sequence":"additional","affiliation":[]},{"given":"Loig","family":"Jezequel","sequence":"additional","affiliation":[]},{"given":"Fabrice","family":"Kordon","sequence":"additional","affiliation":[]},{"given":"Shuo","family":"Li","sequence":"additional","affiliation":[]},{"given":"Emmanuel","family":"Paviot-Adet","sequence":"additional","affiliation":[]},{"given":"Laure","family":"Petrucci","sequence":"additional","affiliation":[]},{"given":"Ji\u0159\u00ed","family":"Srba","sequence":"additional","affiliation":[]},{"given":"Yann","family":"Thierry-Mieg","sequence":"additional","affiliation":[]},{"given":"Karsten","family":"Wolf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,1]]},"reference":[{"key":"3_CR1","unstructured":"Amat, N.: Octant: The Reachability Formula Projector. A tool to project Petri net reachability properties on reduced nets using polyhedral reduction (2023). https:\/\/github.com\/nicolasAmat\/Octant"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Amat, N., Berthomieu, B., Dal\u00a0Zilio, S.: A polyhedral abstraction for petri nets and its application to SMT-based model checking. Fundamenta Informaticae 187(2-4) (2022). https:\/\/doi.org\/10.3233\/FI-222134","DOI":"10.3233\/FI-222134"},{"key":"3_CR3","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-031-06653-5_6","volume-title":"PETRI NETS 2022","author":"N Amat","year":"2022","unstructured":"Amat, N., Chauvet, L.: Kong: a tool to squash concurrent places. In: Bernardinello, L., Petrucci, L. (eds.) PETRI NETS 2022. LNCS, vol. 13288, pp. 115\u2013126. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06653-5_6"},{"key":"3_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-031-27481-7_25","volume-title":"FM 2023","author":"N Amat","year":"2023","unstructured":"Amat, N., Dal Zilio, S.: SMPT: a testbed for reachability methods in generalized Petri nets. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 445\u2013453. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_25"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/978-3-030-99524-9_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Amat","year":"2022","unstructured":"Amat, N., Zilio, S.D., Hujsa, T.: Property directed reachability for generalized petri nets. In: TACAS 2022. LNCS, vol. 13243, pp. 505\u2013523. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_28"},{"key":"3_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-022-00694-8","author":"N Amat","year":"2022","unstructured":"Amat, N., Dal Zilio, S., Le Botlan, D.: Leveraging polyhedral reductions for solving Petri net reachability problems. Int. J. Softw. Tools Technol. Transfer (2022). https:\/\/doi.org\/10.1007\/s10009-022-00694-8","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"3_CR7","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-031-33620-1_18","volume-title":"International Conference on Applications and Theory of Petri Nets and Concurrency","author":"N Amat","year":"2023","unstructured":"Amat, N., Dal Zilio, S., Le Botlan, D.: Automated polyhedral abstraction proving. In: Gomes, L., Lorenz, R. (eds.) PETRI NETS 2023. LNCS, vol. 13929, pp. 324\u2013345. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33620-1_18"},{"issue":"4","key":"3_CR8","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/3543146.3543165","volume":"49","author":"EG Amparore","year":"2022","unstructured":"Amparore, E.G.: Stochastic modelling and evaluation using GreatSPN. ACM SIGMETRICS Perform. Eval. Rev. 49(4), 87\u201391 (2022)","journal-title":"ACM SIGMETRICS Perform. Eval. Rev."},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.laa.2022.06.016","volume":"651","author":"EG Amparore","year":"2022","unstructured":"Amparore, E.G., Ciardo, G., Miner, A.S.: The footprint form of a matrix: definition, properties, and an application. Linear Algebra Appl. 651, 209\u2013229 (2022)","journal-title":"Linear Algebra Appl."},{"issue":"5","key":"3_CR10","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s10009-019-00522-6","volume":"22","author":"EG Amparore","year":"2020","unstructured":"Amparore, E.G., Donatelli, S., Ciardo, G.: Variable order metrics for decision diagrams in system verification. Int. J. Softw. Tools Technol. Transf. 22(5), 541\u2013562 (2020)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR11","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.823","volume":"8","author":"EG Amparore","year":"2022","unstructured":"Amparore, E.G., Donatelli, S., Gall\u00e0, F.: starMC: an automata based CTL* model checker. PeerJ Comput. Sci. 8, e823 (2022)","journal-title":"PeerJ Comput. Sci."},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-36046-6_8","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"M Andersen","year":"2013","unstructured":"Andersen, M., Gatten Larsen, H., Srba, J., Grund S\u00f8rensen, M., Haahr Taankvist, J.: Verification of liveness properties on closed timed-arc petri nets. In: Ku\u010dera, A., Henzinger, T.A., Ne\u0161et\u0159il, J., Vojnar, T., Anto\u0161, D. (eds.) MEMICS 2012. LNCS, vol. 7721, pp. 69\u201381. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36046-6_8"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Babar, J., Miner, A.S.: Meddly: multi-terminal and edge-valued decision diagram library. In: QEST, pp. 195\u2013196. IEEE Computer Society (2010)","DOI":"10.1109\/QEST.2010.34"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"B\u00e9rard, B., et al.: Systems and Software Verification, Model-Checking Techniques and Tools. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/978-3-662-04558-9","DOI":"10.1007\/978-3-662-04558-9"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-319-94111-0_4","volume-title":"Model Checking Software","author":"B Berthomieu","year":"2018","unstructured":"Berthomieu, B., Le Botlan, D., Dal Zilio, S.: Petri net reductions for counting markings. In: Gallardo, M.M., Merino, P. (eds.) SPIN 2018. LNCS, vol. 10869, pp. 65\u201384. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94111-0_4"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Berthomieu, B., Le\u00a0Botlan, D., Dal\u00a0Zilio, S.: Counting petri net markings from reduction equations. Int. J. Softw. Tools Technol. Transfer 22 (2019). https:\/\/doi.org\/10.1007\/s10009-019-00519-1","DOI":"10.1007\/s10009-019-00519-1"},{"issue":"14","key":"3_CR17","doi-asserted-by":"publisher","first-page":"2741","DOI":"10.1080\/00207540412331312688","volume":"42","author":"B Berthomieu","year":"2004","unstructured":"Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA-construction of abstract state spaces for Petri nets and time Petri nets. Int. J. Prod. Res. 42(14), 2741\u20132756 (2004). https:\/\/doi.org\/10.1080\/00207540412331312688","journal-title":"Int. J. Prod. Res."},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Vernadat, F.: Time petri nets analysis with TINA. In: QEST, pp. 123\u2013124. IEEE Computer Society (2006)","DOI":"10.1109\/QEST.2006.56"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-030-89716-1_5","volume-title":"Reachability Problems","author":"A Bilgram","year":"2021","unstructured":"Bilgram, A., Jensen, P.G., Pedersen, T., Srba, J., Taankvist, P.H.: Improvements in unfolding of colored petri nets. In: Bell, P.C., Totzke, P., Potapov, I. (eds.) RP 2021. LNCS, vol. 13035, pp. 69\u201384. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-89716-1_5"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Bilgram, A., Jensen, P., Pedersen, T., Srba, J., Taankvist, P.: Methods for efficient unfolding of colored petri nets. Fundamenta Informaticae 1\u201324 (2023, to appear)","DOI":"10.3233\/FI-222162"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Blondel, V.D., Guillaume, J., Lambiotte, R., Lefebvre, E.: Fast unfolding of community hierarchies in large networks. CoRR abs\/0803.0476 (2008)","DOI":"10.1088\/1742-5468\/2008\/10\/P10008"},{"key":"3_CR22","unstructured":"Bobot, F., Bromberger, M., Hoenicke, J.: The International SMT Competition Web Page (2023). https:\/\/smt-comp.github.io\/"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-319-91268-4_8","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"F B\u00f8nneland","year":"2018","unstructured":"B\u00f8nneland, F., Dyhr, J., Jensen, P.G., Johannsen, M., Srba, J.: Simplification of CTL formulae for efficient model checking of petri nets. In: Khomenko, V., Roux, O.H. (eds.) PETRI NETS 2018. LNCS, vol. 10877, pp. 143\u2013163. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91268-4_8"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-030-85037-1_3","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"FM B\u00f8nneland","year":"2021","unstructured":"B\u00f8nneland, F.M., Jensen, P.G., Larsen, K.G., Mu\u00f1iz, M., Srba, J.: Stubborn set reduction for timed reachability and safety games. In: Dima, C., Shirmohammadi, M. (eds.) FORMATS 2021. LNCS, vol. 12860, pp. 32\u201349. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85037-1_3"},{"issue":"1","key":"3_CR25","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1016\/j.jlamp.2018.09.002","volume":"102","author":"F B\u00f8nneland","year":"2019","unstructured":"B\u00f8nneland, F., Dyhr, J., Jensen, P., Johannsen, M., Srba, J.: Stubborn versus structural reductions for petri nets. J. Log. Algebraic Methods Program. 102(1), 46\u201363 (2019)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"3_CR26","unstructured":"B\u00f8nneland, F., Jensen, P., Larsen, K., Muniz, M., Srba, J.: Partial order reduction for reachability games. In: Proceedings of the 30th International Conference on Concurrency Theory (CONCUR 2019). LIPICS, vol.\u00a0140, pp. 23:1\u201323:15. Dagstuhl Publishing (2019)"},{"key":"3_CR27","unstructured":"Bouvier, P.: The VLSAT-3 Benchmark Suite. Technical report RT-0516, INRIA, Grenoble, France (2021). https:\/\/hal.inria.fr\/hal-3468625. https:\/\/arxiv.org\/abs\/2112.03675"},{"key":"3_CR28","unstructured":"Bouvier, P., Garavel, H.: The VLSAT-1 Benchmark Suite. Technical report RT-0510, INRIA, Grenoble, France (2020). https:\/\/hal.inria.fr\/hal-03007233. https:\/\/arxiv.org\/abs\/2011.11049"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-030-76983-3_17","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"P Bouvier","year":"2021","unstructured":"Bouvier, P., Garavel, H.: Efficient algorithms for three reachability problems in safe petri nets. In: Buchs, D., Carmona, J. (eds.) PETRI NETS 2021. LNCS, vol. 12734, pp. 339\u2013359. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76983-3_17"},{"key":"3_CR30","unstructured":"Bouvier, P., Garavel, H.: The VLSAT-2 Benchmark Suite. Technical report RT-0514, INRIA, Grenoble, France (2021). https:\/\/hal.inria.fr\/hal-03337115. https:\/\/arxiv.org\/abs\/2110.06336"},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Bouvier, P., Garavel, H., Ponce-de-Le\u00f3n, H.: Automatic decomposition of petri nets into automata networks \u2013 a synthetic account. In: Janicki, R., Sidorova, N., Chatain, T. (eds.) PETRI NETS 2020. LNCS, vol. 12152, pp. 3\u201323. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51831-8_1","DOI":"10.1007\/978-3-030-51831-8_1"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-319-91268-4_21","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"D Buchs","year":"2018","unstructured":"Buchs, D., Klikovits, S., Linard, A., Mencattini, R., Racordon, D.: A model checker collection for the model checking contest using docker and machine learning. In: Khomenko, V., Roux, O.H. (eds.) PETRI NETS 2018. LNCS, vol. 10877, pp. 385\u2013395. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91268-4_21"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"698","DOI":"10.1007\/978-3-642-10373-5_36","volume-title":"Formal Methods and Software Engineering","author":"J Byg","year":"2009","unstructured":"Byg, J., J\u00f8rgensen, K.Y., Srba, J.: An efficient translation of timed-arc petri nets to networks of timed automata. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 698\u2013716. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10373-5_36"},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04761-9_7","volume-title":"Automated Technology for Verification and Analysis","author":"J Byg","year":"2009","unstructured":"Byg, J., J\u00f8rgensen, K.Y., Srba, J.: TAPAAL: editor, simulator and verifier of timed-arc petri nets. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 84\u201389. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04761-9_7"},{"issue":"1\u20132","key":"3_CR35","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0304-3975(96)00010-2","volume":"176","author":"G Chiola","year":"1997","unstructured":"Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: A symbolic reachability graph for coloured Petri nets. Theoret. Comput. Sci. 176(1\u20132), 39\u201365 (1997)","journal-title":"Theoret. Comput. Sci."},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/3-540-45319-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Christensen","year":"2001","unstructured":"Christensen, S., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 450\u2013464. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_31"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-030-51831-8_23","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"S Dal Zilio","year":"2020","unstructured":"Dal Zilio, S.: MCC: a tool for unfolding colored petri nets in PNML format. In: Janicki, R., Sidorova, N., Chatain, T. (eds.) PETRI NETS 2020. LNCS, vol. 12152, pp. 426\u2013435. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51831-8_23"},{"issue":"4","key":"3_CR38","first-page":"351","volume":"161","author":"A Dalsgaard","year":"2018","unstructured":"Dalsgaard, A., et al.: A distributed fixed-point algorithm for extended dependency graphs. Fund. Inform. 161(4), 351\u2013381 (2018)","journal-title":"Fund. Inform."},{"key":"3_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-319-57861-3_10","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"AE Dalsgaard","year":"2017","unstructured":"Dalsgaard, A.E., et al.: Extended dependency graphs and efficient distributed fixed-point computation. In: van der Aalst, W., Best, E. (eds.) PETRI NETS 2017. LNCS, vol. 10258, pp. 139\u2013158. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57861-3_10"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-319-47677-3_13","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"AE Dalsgaard","year":"2016","unstructured":"Dalsgaard, A.E., Enevoldsen, S., Larsen, K.G., Srba, J.: Distributed computation of fixed points on dependency graphs. In: Fr\u00e4nzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 197\u2013212. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47677-3_13"},{"key":"3_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-28756-5_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A David","year":"2012","unstructured":"David, A., Jacobsen, L., Jacobsen, M., J\u00f8rgensen, K.Y., M\u00f8ller, M.H., Srba, J.: TAPAAL 2.0: integrated development environment for timed-arc petri nets. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 492\u2013497. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_36"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"David, A., Jacobsen, L., Jacobsen, M., Srba, J.: A forward reachability algorithm for bounded timed-arc Petri nets. In: Proceedings of the 7th International Conference on Systems Software Verification (SSV 2012). EPTCS, vol.\u00a0102, pp. 125\u2013140. Open Publishing Association (2012)","DOI":"10.4204\/EPTCS.102.12"},{"key":"3_CR43","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-031-13188-2_9","volume-title":"CAV 2022","author":"A Duret-Lutz","year":"2022","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13372, pp. 174\u2013187. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9"},{"key":"3_CR44","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-031-32157-3_10","volume-title":"SPIN 2023","author":"EG Henriksen","year":"2023","unstructured":"Henriksen, E.G., et al.: Potency-based heuristic search with randomness for explicit model checking. In: Caltais, G., Schilling, C. (eds.) SPIN 2023. LNCS, vol. 13872, pp. 180\u2013187. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-32157-3_10"},{"key":"3_CR45","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.jlamp.2018.11.005","volume":"104","author":"H Garavel","year":"2019","unstructured":"Garavel, H.: Nested-unit petri nets. J. Log. Algebraic Methods Program. 104, 60\u201385 (2019)","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"1","key":"3_CR46","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.tcs.2005.07.004","volume":"345","author":"J Geldenhuys","year":"2005","unstructured":"Geldenhuys, J., Valmari, A.: More efficient on-the-fly LTL verification with Tarjan\u2019s algorithm. Theor. Comput. Sci. 345(1), 60\u201382 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/3-540-56863-8_52","volume-title":"Application and Theory of Petri Nets 1993","author":"H-M Hanisch","year":"1993","unstructured":"Hanisch, H.-M.: Analysis of place\/transition nets with timed arcs and its application to batch process control. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 282\u2013299. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56863-8_52"},{"issue":"1","key":"3_CR48","doi-asserted-by":"publisher","first-page":"195","DOI":"10.31577\/cai_2021_1_195","volume":"40","author":"C He","year":"2021","unstructured":"He, C., Ding, Z.: More efficient on-the-fly verification methods of colored petri nets. Comput. Inform. 40(1), 195\u2013215 (2021)","journal-title":"Comput. Inform."},{"key":"3_CR49","unstructured":"Hecher, M., Fichte, J.: The Model Counting Competition Web Page (2023). https:\/\/mccompetition.org"},{"key":"3_CR50","unstructured":"Heule, M., Jarvisalo, M., Suda, M., Iser, M., Balyo, T.: The International SAT Competition Web Page (2023). http:\/\/www.satcompetition.org\/"},{"key":"3_CR51","unstructured":"Hillah, L., Kordon, F., Lakos, C., Petrucci, L.: Extending PNML scope: the prioritised petri nets experience. In: Petri Net and Software Engineering (PNSE 2011), Newcastle, UK, vol.\u00a0723, pp. 61\u201375. CEUR (2011)"},{"key":"3_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-15784-4_6","volume-title":"Computer Performance Engineering","author":"L Jacobsen","year":"2010","unstructured":"Jacobsen, L., Jacobsen, M., M\u00f8ller, M.H., Srba, J.: A framework for relating timed transition systems and preserving TCTL model checking. In: Aldini, A., Bernardo, M., Bononi, L., Cortellessa, V. (eds.) EPEW 2010. LNCS, vol. 6342, pp. 83\u201398. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15784-4_6"},{"key":"3_CR53","first-page":"307","volume":"9930","author":"J Jensen","year":"2016","unstructured":"Jensen, J., Nielsen, T., Oestergaard, L., Srba, J.: TAPAAL and reachability analysis of P\/T nets. LNCS Trans. Petri Nets Other Models Concurr. (ToPNoC) 9930, 307\u2013318 (2016)","journal-title":"LNCS Trans. Petri Nets Other Models Concurr. (ToPNoC)"},{"key":"3_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-319-32582-8_9","volume-title":"Model Checking Software","author":"PG Jensen","year":"2016","unstructured":"Jensen, P.G., Larsen, K.G., Srba, J.: Real-time strategy synthesis for timed-arc petri net games via discretization. In: Bo\u0161na\u010dki, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 129\u2013146. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-32582-8_9"},{"key":"3_CR55","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-319-67729-3_15","volume-title":"ICTAC 2017","author":"P Jensen","year":"2017","unstructured":"Jensen, P., Larsen, K., Srba, J.: PTrie: data structure for compressing and storing sets via prefix sharing. In: Hung, D., Kapur, D. (eds.) ICTAC 2017. LNCS, vol. 10580, pp. 248\u2013265. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67729-3_15"},{"key":"3_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-06200-6_26","volume-title":"NASA Formal Methods","author":"PG Jensen","year":"2014","unstructured":"Jensen, P.G., Larsen, K.G., Srba, J., S\u00f8rensen, M.G., Taankvist, J.H.: Memory efficient data structures for explicit verification of timed systems. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 307\u2013312. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_26"},{"key":"3_CR57","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-031-32157-3_9","volume-title":"SPIN 2023","author":"P Jensen","year":"2023","unstructured":"Jensen, P., Larsen, K., Srba, J., Ulrik, N.: Elimination of detached regions in dependency graph verification. In: Caltais, G., Schilling, C. (eds.) SPIN 2023. LNCS, vol. 13872, pp. 163\u2013179. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-32157-3_9"},{"key":"3_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-030-94583-1_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"PG Jensen","year":"2022","unstructured":"Jensen, P.G., Srba, J., Ulrik, N.J., Virenfeldt, S.M.: Automata-driven partial order reduction and guided search for\u00a0LTL model checking. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 151\u2013173. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_8"},{"key":"3_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61"},{"key":"3_CR60","unstructured":"Kordon, F., et al.: Complete Results for the 2023 Edition of the Model Checking Contest (2023). https:\/\/mcc.lip6.fr\/2023\/results.php"},{"key":"3_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/11888116_25","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"F Kordon","year":"2006","unstructured":"Kordon, F., Linard, A., Paviot-Adet, E.: Optimized colored nets unfolding. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 339\u2013355. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11888116_25"},{"issue":"6","key":"3_CR62","doi-asserted-by":"publisher","first-page":"931","DOI":"10.1007\/s10009-021-00615-1","volume":"23","author":"F Kordon","year":"2021","unstructured":"Kordon, F., Hillah, L., Hulin-Hubard, F., Jezequel, L., Paviot-Adet, E.: Study of the efficiency of model checking techniques using results of the MCC from 2015 to 2019. Int. J. Softw. Tools Technol. Transf. 23(6), 931\u2013952 (2021)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-319-77935-5_20","volume-title":"NASA Formal Methods","author":"A Laarman","year":"2018","unstructured":"Laarman, A.: Stubborn transaction reduction. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 280\u2013298. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_20"},{"key":"3_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-31131-4_13","volume-title":"Application and Theory of Petri Nets","author":"A Lehmann","year":"2012","unstructured":"Lehmann, A., Lohmann, N., Wolf, K.: Stubborn sets for simple linear time properties. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol. 7347, pp. 228\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31131-4_13"},{"key":"3_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-030-21571-2_18","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"T Liebke","year":"2019","unstructured":"Liebke, T., Wolf, K.: Taking some burden off an explicit CTL model checker. In: Donatelli, S., Haar, S. (eds.) PETRI NETS 2019. LNCS, vol. 11522, pp. 321\u2013341. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-21571-2_18"},{"key":"3_CR66","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of the 9th ACM Symposium on Principles of Distributed Computing (PODC 1990), pp. 377\u2013410. ACM Press (1990)","DOI":"10.1145\/93385.93442"},{"issue":"1","key":"3_CR67","first-page":"89","volume":"140","author":"J Mateo","year":"2015","unstructured":"Mateo, J., Srba, J., S\u00f8rensen, M.: Soundness of timed-arc workflow nets in discrete and continuous-time semantics. Fund. Inform. 140(1), 89\u2013121 (2015)","journal-title":"Fund. Inform."},{"issue":"9","key":"3_CR68","doi-asserted-by":"publisher","first-page":"1036","DOI":"10.1109\/TCOM.1976.1093424","volume":"24","author":"PM Merlin","year":"1976","unstructured":"Merlin, P.M., Farber, D.J.: Recoverability of communication protocols-implications of a theoretical study. IEEE Trans. Commun. 24(9), 1036\u20131043 (1976)","journal-title":"IEEE Trans. Commun."},{"key":"3_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"3_CR70","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-031-08679-3_11","volume-title":"FORTE 2022","author":"E Paviot-Adet","year":"2022","unstructured":"Paviot-Adet, E., Poitrenaud, D., Renault, E., Thierry-Mieg, Y.: LTL under reductions with weaker conditions than stutter invariance. In: Mousavi, M.R., Philippou, A. (eds.) FORTE 2022. LNCS, vol. 13273, pp. 170\u2013187. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-08679-3_11"},{"issue":"3","key":"3_CR71","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"GL Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"3_CR72","unstructured":"Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. Ph.D. thesis, MIT, USA (1973)"},{"issue":"3","key":"3_CR73","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1023\/A:1008753219837","volume":"15","author":"K Schmidt","year":"1999","unstructured":"Schmidt, K.: Model-checking with coverability graphs. Formal Methods Syst. Des. 15(3), 239\u2013254 (1999)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-48745-X_4","volume-title":"Application and Theory of Petri Nets 1999","author":"K Schmidt","year":"1999","unstructured":"Schmidt, K.: Stubborn sets for standard properties. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 46\u201365. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48745-X_4"},{"issue":"7","key":"3_CR75","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/s002360050002","volume":"36","author":"K Schmidt","year":"2000","unstructured":"Schmidt, K.: How to calculate symmetries of petri nets. Acta Informatica 36(7), 545\u2013590 (2000)","journal-title":"Acta Informatica"},{"key":"3_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-540-24730-2_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Schmidt","year":"2004","unstructured":"Schmidt, K.: Automated generation of a progress measure for the sweep-line method. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 192\u2013204. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_17"},{"key":"3_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-662-46681-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Thierry-Mieg","year":"2015","unstructured":"Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231\u2013237. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_20"},{"key":"3_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-030-51831-8_15","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"Y Thierry-Mieg","year":"2020","unstructured":"Thierry-Mieg, Y.: Structural reductions revisited. In: Janicki, R., Sidorova, N., Chatain, T. (eds.) PETRI NETS 2020. LNCS, vol. 12152, pp. 303\u2013323. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51831-8_15"},{"issue":"3\u20134","key":"3_CR79","first-page":"319","volume":"183","author":"Y Thierry-Mieg","year":"2021","unstructured":"Thierry-Mieg, Y.: Symbolic and structural model-checking. Fundam. Informaticae 183(3\u20134), 319\u2013342 (2021)","journal-title":"Fundam. Informaticae"},{"key":"3_CR80","unstructured":"Thierry-Mieg, Y.: Efficient strategies to compute invariants, bounds and stable places of petri nets. In: PNSE @ Petri Nets. CEUR Workshop Proceedings, vol.\u00a0TBA, pp. 16\u201333. CEUR-WS.org (2023)"},{"key":"3_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-00768-2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Thierry-Mieg","year":"2009","unstructured":"Thierry-Mieg, Y., Poitrenaud, D., Hamez, A., Kordon, F.: Hierarchical set decision diagrams and regular models. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 1\u201315. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_1"},{"key":"3_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491\u2013515. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-53863-1_36"},{"issue":"2\u20134","key":"3_CR83","doi-asserted-by":"publisher","first-page":"245","DOI":"10.3233\/FI-222138","volume":"187","author":"S Wallner","year":"2022","unstructured":"Wallner, S., Wolf, K.: Skeleton abstraction for universal temporal properties. Fundam. Informaticae 187(2\u20134), 245\u2013272 (2022)","journal-title":"Fundam. Informaticae"},{"key":"3_CR84","doi-asserted-by":"crossref","unstructured":"Wimmel, H., Wolf, K.: Applying CEGAR to the petri net state equation. Log. Methods Comput. Sci. 8(3) (2012)","DOI":"10.2168\/LMCS-8(3:27)2012"},{"issue":"2","key":"3_CR85","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/s10270-014-0422-4","volume":"14","author":"K Wolf","year":"2015","unstructured":"Wolf, K.: The petri net twist in explicit model checking. Softw. Syst. Model. 14(2), 711\u2013717 (2015)","journal-title":"Softw. Syst. Model."},{"key":"3_CR86","doi-asserted-by":"crossref","unstructured":"Wolf, K.: Running lola 2.0 in a model checking competition. Trans. Petri Nets Other Model. Concurr. 11, 274\u2013285 (2016)","DOI":"10.1007\/978-3-662-53401-4_13"},{"key":"3_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-319-91268-4_18","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"K Wolf","year":"2018","unstructured":"Wolf, K.: Petri net model checking with LoLA 2. In: Khomenko, V., Roux, O.H. (eds.) PETRI NETS 2018. LNCS, vol. 10877, pp. 351\u2013362. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91268-4_18"},{"key":"3_CR88","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-662-60651-3_2","volume":"14","author":"K Wolf","year":"2019","unstructured":"Wolf, K.: How petri net theory serves petri net model checking: a survey. Trans. Petri Nets Other Model. Concurr. 14, 36\u201363 (2019)","journal-title":"Trans. Petri Nets Other Model. Concurr."},{"key":"3_CR89","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-662-65303-6_5","volume":"16","author":"K Wolf","year":"2022","unstructured":"Wolf, K.: Portfolio management in explicit model checking. Trans. Petri Nets Other Model. Concurr. 16, 91\u2013111 (2022)","journal-title":"Trans. Petri Nets Other Model. Concurr."}],"container-title":["Lecture Notes in Computer Science","TOOLympics Challenge 2023"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-67695-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:13:10Z","timestamp":1750842790000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-67695-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,1]]},"ISBN":["9783031676949","9783031676956"],"references-count":89,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-67695-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,1]]},"assertion":[{"value":"1 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}