{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T23:59:55Z","timestamp":1762300795169,"version":"3.40.3"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711619"},{"type":"electronic","value":"9783031711626"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","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":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Identifying a Markov decision process\u2019s maximal end components is a prerequisite for applying sound probabilistic model checking algorithms. In this paper, we present the first mechanized correctness proof of a maximal end component decomposition algorithm, which is an important algorithm in model checking, using the Isabelle\/HOL theorem prover. We iteratively refine the high-level algorithm and proof into an imperative LLVM bytecode implementation that we integrate into the <jats:sc>Modest Toolset<\/jats:sc> \u2019s existing  model checker. We bring the benefits of interactive theorem proving into practice by reducing the trusted code base of a popular probabilistic model checker and we experimentally show that our new verified maximal end component decomposition in  performs on par with the tool\u2019s previous unverified implementation.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_11","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"206-225","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Efficient Formally Verified Maximal End Component Decomposition for\u00a0MDPs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2908-8838","authenticated-orcid":false,"given":"Bram","family":"Kohlen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3576-0504","authenticated-orcid":false,"given":"Peter","family":"Lammich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"issue":"2","key":"11_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/978-3-319-10575-8_28","volume-title":"Handbook of Model Checking","author":"C Baier","year":"2018","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"key":"11_CR3","unstructured":"Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press (2008)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"issue":"5","key":"11_CR5","first-page":"679","volume":"6","author":"R Bellman","year":"1957","unstructured":"Bellman, R.: A Markovian decision process. J. Math. Mech. 6(5), 679\u2013684 (1957)","journal-title":"J. Math. Mech."},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Biere, A., Van Dijk, T., Heljanko, K.: Hardware model checking competition 2017. In: Stewart, D., Weissenbacher, G., (eds.) 2017 International Conference on Formal Methods in Computer Aided Design FMCAD, p.\u00a09. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102233","DOI":"10.23919\/FMCAD.2017.8102233"},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"1001","DOI":"10.1007\/978-3-319-10575-8_29","volume-title":"Handbook of Model Checking","author":"P Bouyer","year":"2018","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Ouaknine, J., Worrell, J.: Model checking real-time systems. In: Handbook of Model Checking, pp. 1001\u20131046. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_29"},{"issue":"1","key":"11_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-017-9418-4","volume":"60","author":"J Brunner","year":"2018","unstructured":"Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker with partial order reduction. J. Autom. Reasoning 60(1), 3\u201321 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9418-4","journal-title":"J. Autom. Reasoning"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-030-83723-5_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends","author":"CE Budde","year":"2021","unstructured":"Budde, C.E., et al.: On correctness, precision, and performance in quantitative verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12479, pp. 216\u2013241. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-83723-5_15"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, M.: Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: Randall, D. (ed.) 22nd Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 1318\u20131336. SIAM (2011). https:\/\/doi.org\/10.1137\/1.9781611973082.101","DOI":"10.1137\/1.9781611973082.101"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-72308-2_4","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"R Chen","year":"2017","unstructured":"Chen, R., L\u00e9vy, J.-J.: A semi-automatic proof of strong connectivity. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 49\u201365. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-72308-2_4"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-12896-4_358","volume-title":"Logics of Programs","author":"E Clarke","year":"1984","unstructured":"Clarke, E., Mishra, B.: Automatic verification of asynchronous circuits. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 101\u2013115. Springer, Heidelberg (1984). https:\/\/doi.org\/10.1007\/3-540-12896-4_358"},{"key":"11_CR14","unstructured":"Alfaro,L.: Formal verification of probabilistic systems. PhD thesis, Stanford University, USA (1997). https:\/\/searchworks.stanford.edu\/view\/3910936"},{"key":"11_CR15","doi-asserted-by":"publisher","first-page":"1047","DOI":"10.1007\/978-3-319-10575-8_30","volume-title":"Handbook of Model Checking","author":"L Doyen","year":"2018","unstructured":"Doyen, L., Frehse, G., Pappas, G.J., Platzer, A.: Verification of hybrid systems. In: Handbook of Model Checking, pp. 1047\u20131110. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_30"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pp. 342\u2013351. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/LICS.2010.41","DOI":"10.1109\/LICS.2010.41"},{"key":"11_CR17","doi-asserted-by":"publisher","unstructured":"Eisentraut, J., Kelmendi, E., K\u0159et\u00ednsk\u00fd, J., Weininger, M.: Value iteration for simple stochastic games: Stopping criterion and learning algorithm. Inf. Comput. 285(Part), 104886 (2022). https:\/\/doi.org\/10.1016\/J.IC.2022.104886","DOI":"10.1016\/J.IC.2022.104886"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-39799-8_31","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 463\u2013478. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_31"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","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.) FASE 2011. LNCS, vol. 6603, pp. 2\u201317. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19811-3_2"},{"key":"11_CR20","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8219191","author":"K Grover","year":"2023","unstructured":"Grover, K., Weininger, M., Kretinsky, J.: QComp LRA results. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.8219191","journal-title":"Zenodo"},{"key":"11_CR21","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-319-10575-8_18","volume-title":"Handbook of Model Checking","author":"A Gupta","year":"2018","unstructured":"Gupta, A., Kahlon, V., Qadeer, S., Touili, T.: Model checking concurrent programs. In: Handbook of Model Checking, pp. 573\u2013611. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_18"},{"key":"11_CR22","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/J.TCS.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111\u2013131 (2018). https:\/\/doi.org\/10.1016\/J.TCS.2016.12.003","journal-title":"Theor. Comput. Sci."},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-030-99527-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2022","unstructured":"Hartmanns, A.: Correct probabilistic model checking with floating-point arithmetic. In: TACAS 2022. LNCS, vol. 13244, pp. 41\u201359. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_3"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Hartmanns, A.: An overview of Modest models and tools for real stochastic timed systems. In: Dubslaff, C., Luttik, B. (eds.) 5th Workshop on Models for Formal Analysis of Real Systems (MARS), vol. 355 EPTCS, pp. 1\u201312 (2022). https:\/\/doi.org\/10.4204\/EPTCS.355.1","DOI":"10.4204\/EPTCS.355.1"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-54862-8_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2014","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-030-53291-8_26","volume-title":"Computer Aided Verification","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 488\u2013511. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-030-17462-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2019","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 344\u2013350. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20"},{"key":"11_CR28","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Kohlen, B., Lammich, P.: Fast verified SCCs for probabilistic model checking. In: Andr\u00e9, \u00c9., Sun, J. (eds.) 21st International Symposium on Automated Technology for Verification and Analysis (ATVA). LNCS, vol. 14215, pp. 181\u2013202. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_9","DOI":"10.1007\/978-3-031-45329-8_9"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-66107-0_18","volume-title":"Interactive Theorem Proving","author":"M Heule","year":"2017","unstructured":"Heule, M., Hunt, W., Kaufmann, M., Wetzler, N.: Efficient, verified checking of propositional proofs. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 269\u2013284. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_18"},{"issue":"3","key":"11_CR30","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/s10817-016-9401-5","volume":"59","author":"J H\u00f6lzl","year":"2017","unstructured":"H\u00f6lzl, J.: Markov chains and Markov decision processes in Isabelle\/HOL. J. Autom. Reason. 59(3), 345\u2013387 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9401-5","journal-title":"J. Autom. Reason."},{"key":"11_CR31","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1016\/S0065-2458(05)65002-4","volume":"65","author":"GJ Holzmann","year":"2005","unstructured":"Holzmann, G.J.: Software model checking with SPIN. Adv. Comput. 65, 78\u2013109 (2005). https:\/\/doi.org\/10.1016\/S0065-2458(05)65002-4","journal-title":"Adv. Comput."},{"key":"11_CR32","doi-asserted-by":"publisher","unstructured":"Kohlen, B., Hartmanns, A., Lammich, P.: Artifact for the paper \u201cEfficient formally verified maximal end component decomposition for MDPs\u201d. 4TU.ResearchData (2024). https:\/\/doi.org\/10.4121\/3f2a4539-e69b-4d16-b665-530c1abddfbc","DOI":"10.4121\/3f2a4539-e69b-4d16-b665-530c1abddfbc"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Kolobov, A., Mausam, M., Weld, D., Geffner, H.: Heuristic search for generalized stochastic shortest path MDPs. In: Bacchus, F., Domshlak, C., Edelkamp, S., Helmert, M. (eds.) 21st International Conference on Automated Planning and Scheduling (ICAPS). AAAI, (2011). http:\/\/aaai.org\/ocs\/index.php\/ICAPS\/ICAPS11\/paper\/view\/2682","DOI":"10.1609\/icaps.v21i1.13452"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-31424-7_25","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2012","unstructured":"Komuravelli, A., P\u0103s\u0103reanu, C.S., Clarke, E.M.: Assume-guarantee abstraction refinement for probabilistic systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 310\u2013326. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_25"},{"key":"11_CR35","doi-asserted-by":"publisher","unstructured":"K\u0159et\u00ednsk\u00fd, J., Ramneantu, E., Slivinskiy, A., Weininger, M.: Comparison of algorithms for simple stochastic games. Inf. Comput., 289(Part), 104885 (2022). https:\/\/doi.org\/10.1016\/J.IC.2022.104885","DOI":"10.1016\/J.IC.2022.104885"},{"key":"11_CR36","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D. et al.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods Syst. Des., 29(1), 33\u201378, (2006). https:\/\/doi.org\/10.1007\/s10703-006-0005-2","DOI":"10.1007\/s10703-006-0005-2"},{"issue":"1","key":"11_CR37","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"MZ Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101\u2013150 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00046-9","journal-title":"Theor. Comput. Sci."},{"key":"11_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-08970-6_21","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2014","unstructured":"Lammich, P.: Verified efficient implementation of Gabow\u2019s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 325\u2013340. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_21"},{"key":"11_CR39","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Generating verified LLVM from Isabelle\/HOL. In: Harrison,J., Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving (ITP). LIPIcs, vol. 141, pp. 22:1\u201322:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.22","DOI":"10.4230\/LIPIcs.ITP.2019.22"},{"issue":"3","key":"11_CR40","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/s10817-019-09525-z","volume":"64","author":"P Lammich","year":"2020","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. J. Autom. Reason. 64(3), 513\u2013532 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09525-z","journal-title":"J. Autom. Reason."},{"key":"11_CR41","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Refinement of parallel algorithms down to LLVM. In: Andronick, J.,\u00a0Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving (ITP). LIPIcs, vol. 237, pages 24:1\u201324:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.24","DOI":"10.4230\/LIPIcs.ITP.2022.24"},{"key":"11_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-32347-8_12","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 166\u2013182. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_12"},{"key":"11_CR43","doi-asserted-by":"publisher","unstructured":"Sch\u00e4ffeler, M., Abdulaziz, M.: Formally verified solution methods for Markov decision processes. In: 37th AAAI Conference on Artificial Intelligence, pp. 15073\u201315081 (2022). https:\/\/doi.org\/10.1609\/aaai.v37i12.26759","DOI":"10.1609\/aaai.v37i12.26759"},{"key":"11_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-319-12154-3_7","volume-title":"Verified Software: Theories, Tools and Experiments","author":"R Neumann","year":"2014","unstructured":"Neumann, R.: Using Promela in a fully verified executable LTL model checker. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 105\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12154-3_7"},{"key":"11_CR45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0","volume-title":"Logical Foundations of Cyber-Physical Systems","author":"A Platzer","year":"2018","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems. (2018). https:\/\/doi.org\/10.1007\/978-3-319-63588-0"},{"key":"11_CR46","unstructured":"Pottier, F.: Depth-first search and strong connectivity in Coq. In: Vingt-sixi\u00e8mes journ\u00e9es francophones des langages applicatifs (JFLA) (2015)"},{"key":"11_CR47","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":"11_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/978-3-319-96145-3_37","volume-title":"Computer Aided Verification","author":"T Quatmann","year":"2018","unstructured":"Quatmann, T., Katoen, J.-P.: Sound value iteration. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 643\u2013661. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37"},{"key":"11_CR49","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pp. 55\u201374. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"11_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-030-85248-1_16","volume-title":"Formal Methods for Industrial Critical Systems","author":"R Roberts","year":"2021","unstructured":"Roberts, R., et al.: Probabilistic verification for reliability of a two-by-two network-on-chip system. In: Lluch Lafuente, A., Mavridou, A. (eds.) FMICS 2021. LNCS, vol. 12863, pp. 232\u2013248. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_16"},{"key":"11_CR51","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1613\/JAIR.5153","volume":"57","author":"M Steinmetz","year":"2016","unstructured":"Steinmetz, M., Hoffmann, J., Buffet, O.: Goal probability analysis in probabilistic planning: exploring and enhancing the state of the art. J. Artif. Intell. Res. 57, 229\u2013271 (2016). https:\/\/doi.org\/10.1613\/JAIR.5153","journal-title":"J. Artif. Intell. Res."},{"key":"11_CR52","doi-asserted-by":"publisher","unstructured":"Vajjha, K., Shinnar, A., Trager, B., Pestun, V., Fulton, N.: CertRL: formalizing convergence proofs for value and policy iteration in Coq. In: Hritcu, C., Popescu, A. (eds.) 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pp. 18\u201331. ACM, (2021). https:\/\/doi.org\/10.1145\/3437992.3439927","DOI":"10.1145\/3437992.3439927"},{"key":"11_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-23267-6_15","volume-title":"Computer Performance Engineering","author":"F van den Berg","year":"2015","unstructured":"van den Berg, F., Remke, A., Haverkort, B.R.: iDSL: automated performance prediction and analysis of medical imaging systems. In: Beltr\u00e1n, M., Knottenbelt, W., Bradley, J. (eds.) EPEW 2015. LNCS, vol. 9272, pp. 227\u2013242. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23267-6_15"},{"key":"11_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-030-57628-8_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Wimmer","year":"2020","unstructured":"Wimmer, S., Herbreteau, F., van de Pol, J.: Certifying emptiness of timed B\u00fcchi automata. In: Bertrand, N., Jansen, N. (eds.) FORMATS 2020. LNCS, vol. 12288, pp. 58\u201375. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-57628-8_4"},{"key":"11_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-89960-2_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Wimmer","year":"2018","unstructured":"Wimmer, S., Lammich, P.: Verified model checking of timed automata. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 61\u201378. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_4"},{"key":"11_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-030-45190-5_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Wimmer","year":"2020","unstructured":"Wimmer, S., Mutius, J.: Verified certification of reachability checking for timed automata. In: TACAS 2020. LNCS, vol. 12078, pp. 425\u2013443. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_24"},{"key":"11_CR57","doi-asserted-by":"publisher","first-page":"851","DOI":"10.1613\/JAIR.1880","volume":"24","author":"HL Younes","year":"2005","unstructured":"Younes, H.L., Littman, M.L., Weissman, D., Asmuth, J.: The first probabilistic track of the international planning competition. J. Artif. Intell. Res. 24, 851\u2013887 (2005). https:\/\/doi.org\/10.1613\/JAIR.1880","journal-title":"J. Artif. Intell. Res."}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:04:20Z","timestamp":1725933860000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","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":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}