{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:33:10Z","timestamp":1767929590873,"version":"3.49.0"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031827020","type":"print"},{"value":"9783031827037","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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-82703-7_5","type":"book-chapter","created":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T02:16:41Z","timestamp":1737512201000},"page":"97-120","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["1\u20132\u20133\u2013Go! Policy Synthesis for\u00a0Parameterized Markov Decision Processes via\u00a0Decision-Tree Learning and\u00a0Generalization"],"prefix":"10.1007","author":[{"given":"Muqsit","family":"Azeem","sequence":"first","affiliation":[]},{"given":"Debraj","family":"Chakraborty","sequence":"additional","affiliation":[]},{"given":"Sudeep","family":"Kanav","sequence":"additional","affiliation":[]},{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]},{"given":"Mohammadsadegh","family":"Mohagheghi","sequence":"additional","affiliation":[]},{"given":"Stefanie","family":"Mohr","sequence":"additional","affiliation":[]},{"given":"Maximilian","family":"Weininger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,1,23]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Ashok, P., Jackermeier, M., Jagtap, P., Kret\u00ednsk\u00fd, J., Weininger, M., Zamani, M.: dtControl: decision tree learning algorithms for controller representation. In: Ames, A.D., Seshia, S.A., Deshmukh, J. (eds.) HSCC \u201920: 23rd ACM International Conference on Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia, April 21\u201324, 2020, pp. 30:1\u201330:2. ACM (2020). https:\/\/doi.org\/10.1145\/3365365.3383468","DOI":"10.1145\/3365365.3383468"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Ashok, P., Jackermeier, M., Kret\u00ednsk\u00fd, J., Weinhuber, C., Weininger, M., Yadav, M.: dtControl 2.0: explainable strategy representation via decision tree learning steered by experts. In: TACAS (2). Lecture Notes in Computer Science, vol. 12652, pp. 326\u2013345. Springer (2021)","DOI":"10.1007\/978-3-030-72013-1_17"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-030-25540-4_29","volume-title":"Computer Aided Verification","author":"P Ashok","year":"2019","unstructured":"Ashok, P., K\u0159et\u00ednsk\u00fd, J., Weininger, M.: PAC statistical model checking for Markov decision processes and stochastic games. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 497\u2013519. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_29"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Azeem, M., Chakraborty, D., Kanav, S., Kret\u00ednsk\u00fd, J., Mohagheghi, M., Mohr, S., Weininger, M.: 1-2-3-Go! policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. CoRR abs\/2410.18293 (2024). https:\/\/arxiv.org\/abs\/2410.18293","DOI":"10.1007\/978-3-031-82703-7_5"},{"key":"5_CR5","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-63387-9_8","volume-title":"Computer Aided Verification","author":"C Baier","year":"2017","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 160\u2013180. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8"},{"issue":"1","key":"5_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2019","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-319-21690-4_10","volume-title":"Computer Aided Verification","author":"T Br\u00e1zdil","year":"2015","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmel\u00edk, M., Fellner, A., K\u0159et\u00ednsk\u00fd, J.: Counterexample explanation by learning small strategies in Markov decision processes. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 158\u2013177. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_10"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., et al.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"key":"5_CR10","unstructured":"Breiman, L.: Classification and Regression Trees. The Wadsworth statistics \/ probability series), Wadsworth International Group (1984)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-319-89963-3_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2018","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: A statistical model checker for nondeterminism and rare events. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 340\u2013358. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_20"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Budde, C.E., et al.: On correctness, precision, and performance in quantitative verification - QComp 2020 competition report. In: ISoLA (4). Lecture Notes in Computer Science, vol. 12479, pp. 216\u2013241. Springer (2020)","DOI":"10.1007\/978-3-030-83723-5_15"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Ciesinski, F., Baier, C., Gr\u00f6\u00dfer, M., Klein, J.: Reduction techniques for model checking markov decision processes. In: QEST, pp. 45\u201354. IEEE Computer Society (2008)","DOI":"10.1109\/QEST.2008.45"},{"issue":"26","key":"5_CR14","doi-asserted-by":"publisher","first-page":"726","DOI":"10.21105\/joss.00726","volume":"3","author":"RR Curtin","year":"2018","unstructured":"Curtin, R.R., Edel, M., Lozhnikov, M., Mentekidis, Y., Ghaisas, S., Zhang, S.: mlpack 3: a fast, flexible machine learning library. J. Open Source Softw. 3(26), 726 (2018)","journal-title":"J. Open Source Softw."},{"issue":"4","key":"5_CR15","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/s10009-015-0383-0","volume":"17","author":"PR D\u2019Argenio","year":"2015","unstructured":"D\u2019Argenio, P.R., Legay, A., Sedwards, S., Traonouez, L.: Smart sampling for lightweight verification of Markov decision processes. Int. J. Softw. Tools Technol. Transf. 17(4), 469\u2013484 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR16","unstructured":"Feng, L.: On learning assumptions for compositional verification of probabilistic systems. Ph.D. thesis, University of Oxford, UK (2014)"},{"key":"5_CR17","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-19811-3_2","volume-title":"Fundamental Approaches to Software Engineering","author":"L Feng","year":"2011","unstructured":"Feng, L., Kwiatkowska, M., Parker, D.: Automated learning of probabilistic assumptions for compositional reasoning. In: Giannakopoulou, D., Orejas, F. (eds.) Fundamental Approaches to Software Engineering, pp. 2\u201317. Springer, Heidelberg (2011)"},{"issue":"9","key":"5_CR18","doi-asserted-by":"publisher","first-page":"131","DOI":"10.3390\/a11090131","volume":"11","author":"JF Groote","year":"2018","unstructured":"Groote, J.F., Verduzco, J.R., de Vink, E.P.: An efficient algorithm to determine probabilistic bisimulation. Algorithms 11(9), 131 (2018)","journal-title":"Algorithms"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-030-50086-3_6","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"TP Gros","year":"2020","unstructured":"Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., Steinmetz, M.: Deep statistical model checking. In: Gotsman, A., Sokolova, A. (eds.) FORTE 2020. LNCS, vol. 12136, pp. 96\u2013114. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50086-3_6"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Gr\u00f6\u00dfer, M., Baier, C.: Partial order reduction for Markov decision processes: a survey. In: FMCO. Lecture Notes in Computer Science, vol.\u00a04111, pp. 408\u2013427. Springer (2005)","DOI":"10.1007\/11804192_19"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-11439-2_10","volume-title":"Reachability Problems","author":"S Haddad","year":"2014","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: refining convergence of value iteration. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 125\u2013137. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_10"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-030-17462-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EM Hahn","year":"2019","unstructured":"Hahn, E.M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., Wojtczak, D.: Omega-regular objectives in model-free reinforcement learning. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 395\u2013412. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_27"},{"key":"5_CR23","unstructured":"Hartmanns, A.: MODEST - A unified language for quantitative models. In: FDL, pp. 44\u201351. IEEE (2012). https:\/\/ieeexplore.ieee.org\/document\/6336982\/"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: Explicit model checking of very large MDP using partitioning and secondary storage. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12\u201315, 2015, Proceedings. Lecture Notes in Computer Science, vol.\u00a09364, pp. 131\u2013147. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_10","DOI":"10.1007\/978-3-319-24953-7_10"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: TACAS (1). Lecture Notes in Computer Science, vol. 11427, pp. 344\u2013350. Springer (2019).https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20","DOI":"10.1007\/978-3-030-17462-0_20"},{"issue":"4","key":"5_CR26","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/s10009-014-0349-7","volume":"17","author":"A Hartmanns","year":"2015","unstructured":"Hartmanns, A., Timmer, M.: Sound statistical model checking for MDP using partial order and confluence reduction. Int. J. Softw. Tools Technol. Transf. 17(4), 429\u2013456 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Henriques, D., Martins, J.G., Zuliani, P., Platzer, A., Clarke, E.M.: Statistical model checking for Markov decision processes. In: QEST. pp. 84\u201393. IEEE Computer Society (2012)","DOI":"10.1109\/QEST.2012.19"},{"issue":"4","key":"5_CR28","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/s10009-021-00633-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1","key":"5_CR29","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/0020-0190(76)90095-8","volume":"5","author":"L Hyafil","year":"1976","unstructured":"Hyafil, L., Rivest, R.L.: Constructing optimal binary decision trees is np-complete. Inf. Process. Lett. 5(1), 15\u201317 (1976). https:\/\/doi.org\/10.1016\/0020-0190(76)90095-8","journal-title":"Inf. Process. Lett."},{"key":"5_CR30","unstructured":"Kamaleson, N.: Model reduction techniques for probabilistic verification of Markov chains. Ph.D. thesis, University of Birmingham, UK (2018)"},{"issue":"2","key":"5_CR31","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10009-017-0456-3","volume":"20","author":"J Klein","year":"2018","unstructured":"Klein, J., et al.: Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic b\u00fcchi automata. Int. J. Softw. Tools Technol. Transf. 20(2), 179\u2013194 (2018)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-319-47166-2_3","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"J K\u0159et\u00ednsk\u00fd","year":"2016","unstructured":"K\u0159et\u00ednsk\u00fd, J.: Survey of statistical verification of linear unbounded properties: model checking and distances. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 27\u201345. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_3"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Of cores: a partial-exploration framework for Markov decision processes. Log. Methods Comput. Sci. 16(4) (2020)","DOI":"10.23638\/LMCS-16(4:3)2020"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation: Modelling Techniques and Tools","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200\u2013204. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46029-2_13"},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: QEST, pp. 157\u2013166. IEEE Computer Society (2006)","DOI":"10.1109\/QEST.2006.19"},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/11817963_23","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 234\u2013248. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_23"},{"key":"5_CR37","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST, pp. 203\u2013204. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/QEST.2012.14","DOI":"10.1109\/QEST.2012.14"},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Parker, D., Qu, H.: Incremental quantitative verification for markov decision processes. In: DSN, pp. 359\u2013370. IEEE Compute Society (2011)","DOI":"10.1109\/DSN.2011.5958249"},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"Li, R., Liu, Y.: Compositional stochastic model checking probabilistic automata via symmetric assume-guarantee rule. In: 2019 IEEE 17th International Conference on Software Engineering Research, Management and Applications (SERA), pp. 110\u2013115. IEEE (2019)","DOI":"10.1109\/SERA.2019.8886808"},{"key":"5_CR40","unstructured":"Lomuscio, A., Pirovano, E.: A counter abstraction technique for the verification of probabilistic swarm systems. In: AAMAS, pp. 161\u2013169. International Foundation for Autonomous Agents and Multiagent Systems (2019)"},{"key":"5_CR41","unstructured":"Maisonneuve, V.: Automatic heuristic-based generation of MTBDD variable orderings for prism models. internship report (2009)"},{"key":"5_CR42","unstructured":"Mitchell, T.: Machine Learning, vol.\u00a01. McGraw-Hill, New York (1997)"},{"key":"5_CR43","unstructured":"Mohagheghi, M., Salehi, K.: Machine learning and disk-based methods for qualitative verification of Markov decision processes. In: ICTERI Workshops. CEUR Workshop Proceedings, vol.\u00a02732, pp. 74\u201388. CEUR-WS.org (2020)"},{"key":"5_CR44","unstructured":"Parker, D.A.: Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis, University of Birmingham, UK (2003)"},{"key":"5_CR45","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994). https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"key":"5_CR46","unstructured":"Pyeatt, L.D., Howe, A.E.: Decision tree function approximation in reinforcement learning (1999)"},{"issue":"4","key":"5_CR47","doi-asserted-by":"publisher","first-page":"443","DOI":"10.3233\/FI-2018-1637","volume":"157","author":"A Rataj","year":"2018","unstructured":"Rataj, A., Wozna-Szczesniak, B.: Extrapolation of an optimal policy using statistical probabilistic model checking. Fundam. Informaticae 157(4), 443\u2013461 (2018)","journal-title":"Fundam. Informaticae"},{"issue":"3","key":"5_CR48","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1002\/j.1538-7305.1948.tb01338.x","volume":"27","author":"CE Shannon","year":"1948","unstructured":"Shannon, C.E.: A mathematical theory of communication. The Bell system technical journal 27(3), 379\u2013423 (1948)","journal-title":"The Bell system technical journal"},{"key":"5_CR49","doi-asserted-by":"crossref","unstructured":"Smolka, S., et al.: Scalable verification of probabilistic networks. In: PLDI, pp. 190\u2013203. ACM (2019)","DOI":"10.1145\/3314221.3314639"},{"key":"5_CR50","unstructured":"Sutton, R.S., Barto, A.G.: Introduction to Reinforcement Learning, 1st edn. Cambridge, MA, USA (1998)"},{"key":"5_CR51","doi-asserted-by":"crossref","unstructured":"Tappler, M., Aichernig, B.K., Bacci, G., Eichlseder, M., Larsen, K.G.: L$$ ^{\\text{*}}$$-based learning of Markov decision processes. In: FM. Lecture Notes in Computer Science, vol. 11800, pp. 651\u2013669. Springer (2019)","DOI":"10.1007\/978-3-030-30942-8_38"},{"key":"5_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223\u2013235. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_17"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-82703-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T06:13:56Z","timestamp":1763705636000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-82703-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031827020","9783031827037"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-82703-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 January 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denver, CO","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 January 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 January 2025","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":"vmcai2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}