{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:16:36Z","timestamp":1770977796499,"version":"3.50.1"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906527","type":"print"},{"value":"9783031906534","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"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>\n                  <jats:p>\n                    The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are\n                    <jats:italic>certificates<\/jats:italic>\n                    \u2014lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of\n                    <jats:italic>Markov decision processes<\/jats:italic>\n                    (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for\n                    <jats:italic>arbitrary<\/jats:italic>\n                    finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in  and provide a\n                    <jats:italic>formally verified certificate checker<\/jats:italic>\n                    . Moreover, we augment existing algorithms in the probabilistic model checker  with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-90653-4_7","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T08:04:24Z","timestamp":1746173064000},"page":"130-151","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Fixed Point Certificates for Reachability and Expected Rewards in MDPs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4561-241X","authenticated-orcid":false,"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2843-5511","authenticated-orcid":false,"given":"Tim","family":"Quatmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2612-2335","authenticated-orcid":false,"given":"Maximilian","family":"Sch\u00e4ffeler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0163-2152","authenticated-orcid":false,"given":"Maximilian","family":"Weininger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1084-6408","authenticated-orcid":false,"given":"Tobias","family":"Winkler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-7221-2554","authenticated-orcid":false,"given":"Daniel","family":"Zilken","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Stochastic omega-regular verification and control with supermartingales. In: CAV (3). Lecture Notes in Computer Science, vol. 14683, pp. 395\u2013419. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_18","DOI":"10.1007\/978-3-031-65633-0_18"},{"key":"7_CR2","unstructured":"de\u00a0Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University, USA (1997)"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Andriushchenko, R., Bork, A., Budde, C.E., \u010ce\u0161ka, M., Hahn, E.M., Hartmanns, A., Israelsen, B., Jansen, N., Jeppson, J., Junges, S., K\u00f6hl, M.A., K\u00f6nighofer, B., K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Parker, D., Pranger, S., Quatmann, T., Ruijters, E., Taylor, L., Volk, M., Weininger, M., Zhang, Z.: Tools at the frontiers of quantitative verification: QComp 2023 competition report. In: International TOOLympics Challenge, pp. 90\u2013146. Springer (2024)","DOI":"10.1007\/978-3-031-67695-6_4"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Azeem, M., Evangelidis, A., Kret\u00ednsk\u00fd, J., Slivinskiy, A., Weininger, M.: Optimistic and topological value iteration for simple stochastic games. In: ATVA. Lecture Notes in Computer Science, vol. 13505, pp. 285\u2013302. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_18","DOI":"10.1007\/978-3-031-19992-9_18"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Baier, C., de\u00a0Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Baier, C., Chau, C., Kl\u00fcppelholz, S.: Certificates and witnesses for multi-objective queries in Markov decision processes. In: QEST+FORMATS. Lecture Notes in Computer Science, vol. 14996, pp. 1\u201318. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-68416-6_1","DOI":"10.1007\/978-3-031-68416-6_1"},{"key":"7_CR7","unstructured":"Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)"},{"key":"7_CR8","doi-asserted-by":"publisher","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: CAV (1). Lecture Notes in Computer Science, vol. 10426, pp. 160\u2013180. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"7_CR9","unstructured":"Balyo, T., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M.: Proceedings of SAT Competition 2023: Solver, benchmark and proof checker descriptions (2023), https:\/\/researchportal.helsinki.fi\/en\/publications\/proceedings-of-sat-competition-2023-solver-benchmark-and-proof-ch"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Batz, K., Biskup, T.J., Katoen, J., Winkler, T.: Programmatic strategy synthesis: Resolving nondeterminism in probabilistic programs. Proc. ACM Program. Lang. 8(POPL), 2792\u20132820 (2024). https:\/\/doi.org\/10.1145\/3632935","DOI":"10.1145\/3632935"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Bellman, R.: Dynamic programming and stochastic control processes. Inf. Control. 1(3), 228\u2013239 (1958). https:\/\/doi.org\/10.1016\/S0019-9958(58)80003-0","DOI":"10.1016\/S0019-9958(58)80003-0"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: TACAS (2). Lecture Notes in Computer Science, vol. 13994, pp. 495\u2013522. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kret\u00ednsk\u00fd, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: ATVA. Lecture Notes in Computer Science, vol.\u00a08837, pp. 98\u2013114. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: TACAS (2). Lecture Notes in Computer Science, vol. 10206, pp. 151\u2013168 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Hartmanns, A., Klauck, M., Kret\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Turrini, A., Zhang, Z.: 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). https:\/\/doi.org\/10.1007\/978-3-030-83723-5_15","DOI":"10.1007\/978-3-030-83723-5_15"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, T.A.: Value iteration. In: 25 Years of Model Checking. Lecture Notes in Computer Science, vol.\u00a05000, pp. 107\u2013138. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-69850-0_7","DOI":"10.1007\/978-3-540-69850-0_7"},{"key":"7_CR17","unstructured":"Chatterjee, K., Quatmann, T., Sch\u00e4ffeler, M., Weininger, M., Winkler, T., Zilken, D.: Fixed point certificates for reachability and expected rewards in MDPs. CoRR abs\/2501.11467 (2025), https:\/\/arxiv.org\/abs\/2501.11467"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Quatmann, T., Sch\u00e4ffeler, M., Weininger, M., Winkler, T., Zillken, D.: Artifact: Fixed point certificates for reachability and expected rewards in mdps (2025). https:\/\/doi.org\/10.5281\/zenodo.14626585","DOI":"10.5281\/zenodo.14626585"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M.Z., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Des. 43(1), 61\u201392 (2013). https:\/\/doi.org\/10.1007\/S10703-013-0183-7, https:\/\/doi.org\/10.1007\/s10703-013-0183-7","DOI":"10.1007\/S10703-013-0183-7"},{"key":"7_CR20","unstructured":"Debbi, H.: Counterexamples in model checking - A survey. Informatica (Slovenia) 42(2) (2018), http:\/\/www.informatica.si\/index.php\/informatica\/article\/view\/1442"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Froleyks, N., Yu, E., Biere, A., Heljanko, K.: Certifying phase abstraction. In: IJCAR (1). Lecture Notes in Computer Science, vol. 14739, pp. 284\u2013303. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_17","DOI":"10.1007\/978-3-031-63498-7_17"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Funke, F., Jantsch, S., Baier, C.: Farkas certificates and minimal witnesses for probabilistic reachability constraints. In: TACAS (1). Lecture Notes in Computer Science, vol. 12078, pp. 324\u2013345. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_18","DOI":"10.1007\/978-3-030-45190-5_18"},{"key":"7_CR23","unstructured":"Granlund, T., Team, G.D.: GNU MP 6.0 Multiple Precision Arithmetic Library. Samurai Media Limited (2015)"},{"key":"7_CR24","doi-asserted-by":"publisher","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","DOI":"10.1016\/J.TCS.2016.12.003"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"Haftmann, F., Krauss, A., Kuncar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: ITP. Lecture Notes in Computer Science, vol.\u00a07998, pp. 100\u2013115. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_10","DOI":"10.1007\/978-3-642-39634-2_10"},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Hartmanns, A., Hensel, C., Klauck, M., Klein, J., Kret\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Ruijters, E., Steinmetz, M.: The 2019 comparison of tools for the analysis of quantitative formal models - (QComp 2019 competition report). In: TACAS (3). Lecture Notes in Computer Science, vol. 11429, pp. 69\u201392. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_5","DOI":"10.1007\/978-3-030-17502-3_5"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Hartmanns, A.: Correct probabilistic model checking with floating-point arithmetic. In: TACAS (2). Lecture Notes in Computer Science, vol. 13244, pp. 41\u201359. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_3","DOI":"10.1007\/978-3-030-99527-0_3"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: An integrated environment for quantitative modelling and verification. In: TACAS. LNCS, vol.\u00a08413, pp. 593\u2013598. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner\u2019s guide to MDP model checking algorithms. In: TACAS (1). Lecture Notes in Computer Science, vol. 13993, pp. 469\u2013488. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_24","DOI":"10.1007\/978-3-031-30823-9_24"},{"key":"7_CR30","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: The revised practitioner\u2019s guide to MDP model checking algorithms. Under submission, Preprint: https:\/\/sjunges.github.io\/files\/revised_practitioners_guide.pdf (2025)"},{"key":"7_CR31","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: CAV (2). Lecture Notes in Computer Science, vol. 12225, pp. 488\u2013511. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"7_CR32","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"},{"key":"7_CR33","doi-asserted-by":"crossref","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). 10.1007\/S10009-021-00633-Z","DOI":"10.1007\/s10009-021-00633-z"},{"key":"7_CR34","doi-asserted-by":"publisher","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","DOI":"10.1007\/S10817-016-9401-5"},{"key":"7_CR35","unstructured":"Jantsch, S.: Certificates and Witnesses for Probabilistic Model Checking. Ph.D. thesis, Dresden University of Technology, Germany (2022)"},{"key":"7_CR36","doi-asserted-by":"publisher","unstructured":"Jantsch, S., Harder, H., Funke, F., Baier, C.: SWITSS: Computing small witnessing subsystems. In: FMCAD. pp. 236\u2013244. IEEE (2020). https:\/\/doi.org\/10.34727\/2020\/ISBN.978-3-85448-042-6_31","DOI":"10.34727\/2020\/ISBN.978-3-85448-042-6_31"},{"key":"7_CR37","doi-asserted-by":"publisher","unstructured":"Junges, S., Katoen, J., P\u00e9rez, G.A., Winkler, T.: The complexity of reachability in parametric Markov decision processes. J. Comput. Syst. Sci. 119, 183\u2013210 (2021). https:\/\/doi.org\/10.1016\/J.JCSS.2021.02.006","DOI":"10.1016\/J.JCSS.2021.02.006"},{"key":"7_CR38","doi-asserted-by":"publisher","unstructured":"Kratsch, D., McConnell, R.M., Mehlhorn, K., Spinrad, J.P.: Certifying algorithms for recognizing interval graphs and permutation graphs. SIAM J. Comput. 36(2), 326\u2013353 (2006). https:\/\/doi.org\/10.1137\/S0097539703437855","DOI":"10.1137\/S0097539703437855"},{"key":"7_CR39","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Weininger, M.: Stopping criteria for value iteration on stochastic games with quantitative objectives. In: LICS. pp. 1\u201314. IEEE (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175771","DOI":"10.1109\/LICS56636.2023.10175771"},{"key":"7_CR40","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Sickert, S.: Certifying inexpressibility. In: FoSSaCS. Lecture Notes in Computer Science, vol. 12650, pp. 385\u2013405. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-71995-1_20","DOI":"10.1007\/978-3-030-71995-1_20"},{"key":"7_CR41","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: From complementation to certification. Theor. Comput. Sci. 345(1), 83\u2013100 (2005). https:\/\/doi.org\/10.1016\/J.TCS.2005.07.021","DOI":"10.1016\/J.TCS.2005.07.021"},{"key":"7_CR42","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: CAV. Lecture Notes in Computer Science, vol.\u00a06806, pp. 585\u2013591. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"7_CR43","doi-asserted-by":"publisher","unstructured":"Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T.A.: Stability verification in stochastic control systems via neural network supermartingales. In: AAAI. pp. 7326\u20137336. AAAI Press (2022). https:\/\/doi.org\/10.1609\/AAAI.V36I7.20695","DOI":"10.1609\/AAAI.V36I7.20695"},{"key":"7_CR44","doi-asserted-by":"publisher","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119\u2013161 (2011). https:\/\/doi.org\/10.1016\/J.COSREV.2010.09.009","DOI":"10.1016\/J.COSREV.2010.09.009"},{"key":"7_CR45","doi-asserted-by":"publisher","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: CAV. Lecture Notes in Computer Science, vol.\u00a02102, pp. 2\u201313. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_2","DOI":"10.1007\/3-540-44585-4_2"},{"key":"7_CR46","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol.\u00a02283. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9, https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"7_CR47","doi-asserted-by":"publisher","unstructured":"Peled, D.A., Pnueli, A., Zuck, L.D.: From falsification to verification. In: FSTTCS. Lecture Notes in Computer Science, vol.\u00a02245, pp. 292\u2013304. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-45294-X_25","DOI":"10.1007\/3-540-45294-X_25"},{"key":"7_CR48","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":"7_CR49","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.: Sound value iteration. In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 643\u2013661. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"7_CR50","doi-asserted-by":"publisher","unstructured":"Sch\u00e4ffeler, M., Abdulaziz, M.: Formally verified solution methods for Markov decision processes. In: AAAI. pp. 15073\u201315081. AAAI Press (2023). https:\/\/doi.org\/10.1609\/AAAI.V37I12.26759","DOI":"10.1609\/AAAI.V37I12.26759"},{"key":"7_CR51","doi-asserted-by":"publisher","unstructured":"Takisaka, T., Zhang, L., Wang, C., Liu, J.: Lexicographic ranking supermartingales with lazy lower bounds. In: CAV (3). Lecture Notes in Computer Science, vol. 14683, pp. 420\u2013442. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_19","DOI":"10.1007\/978-3-031-65633-0_19"},{"key":"7_CR52","doi-asserted-by":"publisher","unstructured":"Tan, Y.K., Yang, J., Soos, M., Myreen, M.O., Meel, K.S.: Formally certified approximate model counting. In: CAV (1). Lecture Notes in Computer Science, vol. 14681, pp. 153\u2013177. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_8","DOI":"10.1007\/978-3-031-65627-9_8"},{"key":"7_CR53","doi-asserted-by":"publisher","unstructured":"White, D.J.: A survey of applications of Markov decision processes. Journal of the operational research society 44(11), 1073\u20131096 (1993). https:\/\/doi.org\/10.1057\/jors.1993.181","DOI":"10.1057\/jors.1993.181"},{"key":"7_CR54","doi-asserted-by":"publisher","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Katoen, J., Becker, B.: Minimal counterexamples for linear-time probabilistic verification. Theor. Comput. Sci. 549, 61\u2013100 (2014). https:\/\/doi.org\/10.1016\/J.TCS.2014.06.020, https:\/\/doi.org\/10.1016\/j.tcs.2014.06.020","DOI":"10.1016\/J.TCS.2014.06.020"},{"key":"7_CR55","doi-asserted-by":"publisher","unstructured":"Winkler, T., Katoen, J.: Certificates for probabilistic pushdown automata via optimistic value iteration. In: TACAS (2). Lecture Notes in Computer Science, vol. 13994, pp. 391\u2013409. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_24","DOI":"10.1007\/978-3-031-30820-8_24"},{"key":"7_CR56","doi-asserted-by":"publisher","unstructured":"Winkler, T., Katoen, J.: On certificates, expected runtimes, and termination in probabilistic pushdown automata. In: LICS. pp. 1\u201313. IEEE (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175714","DOI":"10.1109\/LICS56636.2023.10175714"},{"key":"7_CR57","doi-asserted-by":"publisher","unstructured":"Yu, E., Biere, A., Heljanko, K.: Progress in certifying hardware model checking results. In: CAV (2). Lecture Notes in Computer Science, vol. 12760, pp. 363\u2013386. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_17","DOI":"10.1007\/978-3-030-81688-9_17"},{"key":"7_CR58","doi-asserted-by":"publisher","unstructured":"Yu, E., Froleyks, N., Biere, A., Heljanko, K.: Stratified certification for k-induction. In: FMCAD. pp. 59\u201364. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_11","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_11"},{"key":"7_CR59","doi-asserted-by":"publisher","unstructured":"Yu, E., Froleyks, N., Biere, A., Heljanko, K.: Towards compositional hardware model checking certification. In: FMCAD. pp. 1\u201311. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/ISBN.978-3-85448-060-0_12","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_12"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90653-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:36:42Z","timestamp":1764401802000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90653-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906527","9783031906534"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90653-4_7","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":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}