{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T10:05:00Z","timestamp":1767261900564,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032095237","type":"print"},{"value":"9783032095244","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T00:00:00Z","timestamp":1762300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T00:00:00Z","timestamp":1762300800000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-09524-4_13","type":"book-chapter","created":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T21:14:08Z","timestamp":1762290848000},"page":"186-201","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["DTMC Model Checking by\u00a0Path Abstraction Revisited"],"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\/0009-0002-9198-3809","authenticated-orcid":false,"given":"Robert","family":"Modderman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,5]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"\u00c1brah\u00e1m, E., Jansen, N., Wimmer, R., Katoen, J.P., Becker, B.: DTMC model checking by SCC reduction. In: 7th International Conference on the Quantitative Evaluation of Systems, pp. 37\u201346. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/QEST.2010.13","DOI":"10.1109\/QEST.2010.13"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Andr\u00e9s, M.E., D\u2019Argenio, P., van Rossum, P.: Significant diagnostic counterexamples in probabilistic model checking. In: Chockler, H., Hu, A.J. (eds.) Hardware and Software: Verification and Testing. LNCS, vol. 5394, pp. 129\u2013148. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-01702-5_15","DOI":"10.1007\/978-3-642-01702-5_15"},{"key":"13_CR3","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Ciesinski, F., Baier, C., Gr\u00f6\u00dfer, M., Klein, J.: Reduction techniques for model checking Markov decision processes. In: 5th International Conference on the Quantitative Evaluation of Systems (QEST 2008), pp. 45\u201354. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/QEST.2008.45","DOI":"10.1109\/QEST.2008.45"},{"key":"13_CR5","unstructured":"Dai, P., Goldsmith, J.: Topological value iteration algorithm for Markov decision processes. In: Veloso, M.M. (ed.) 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 1860\u20131865 (2007). http:\/\/ijcai.org\/Proceedings\/07\/Papers\/300.pdf"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-31862-0_21","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"C Daws","year":"2005","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280\u2013294. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31862-0_21"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53\u2013113. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21455-4_3"},{"key":"13_CR8","unstructured":"Guen, H.L., Marie, R.A.: Visiting probabilities in non-irreducible Markov chains with strongly connected components. In: Amborski, K., Meuth, H. (eds.) 16th European Simulation Multiconference: Modelling and Simulation 2002, pp. 548\u2013552. SCS Europe (2002)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-319-11737-9_12","volume-title":"Formal Methods and Software Engineering","author":"L Gui","year":"2014","unstructured":"Gui, L., Sun, J., Song, S., Liu, Y., Dong, J.S.: SCC-based improved reachability analysis for Markov decision processes. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 171\u2013186. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11737-9_12"},{"issue":"1","key":"13_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/S10009-010-0146-X","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transf. 13(1), 3\u201319 (2011). https:\/\/doi.org\/10.1007\/S10009-010-0146-X","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR11","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-24953-7_10","volume-title":"Automated Technology for Verification and Analysis","author":"A Hartmanns","year":"2015","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.) ATVA 2015. LNCS, vol. 9364, pp. 131\u2013147. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_10"},{"key":"13_CR13","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 2023). LNCS, vol. 14215, pp. 181\u2013202. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_9","DOI":"10.1007\/978-3-031-45329-8_9"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Kohlen, B., Lammich, P.: Efficient formally verified maximal end component decomposition for MDPs. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) 26th International Formal Methods Symposium (FM 2024). LNCS, vol. 14933, pp. 206\u2013225. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_11","DOI":"10.1007\/978-3-031-71162-6_11"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Modderman, R.: DTMC model checking by path abstraction revisited (extended version). CoRR abs\/2509.02393 (2025). https:\/\/doi.org\/10.48550\/arXiv.2509.02393","DOI":"10.48550\/arXiv.2509.02393"},{"issue":"4","key":"13_CR16","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.P., 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."},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Jansen, N., Corzilius, F., Volk, M., Wimmer, R., \u00c1brah\u00e1m, E., Katoen, J.P., Becker, B.: Accelerating parametric probabilistic verification. In: Norman, G., Sanders, W.H. (eds.) 11th International Conference on the Quantitative Evaluation of Systems (QEST 2014). LNCS, vol.\u00a08657, pp. 404\u2013420. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-10696-0_31","DOI":"10.1007\/978-3-319-10696-0_31"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Kohlen, B., Sch\u00e4ffeler, M., Abdulaziz, M., Hartmanns, A., Lammich, P.: A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. In: Piskac, R., Rakamaric, Z. (eds.) 37th International Conference on Computer Aided Verification (CAV 2025). LNCS, vol. 15932, pp. 122\u2013146. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98679-6_6","DOI":"10.1007\/978-3-031-98679-6_6"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Parker, D., Qu, H.: Incremental quantitative verification for Markov decision processes. In: 2011 IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN 2011), pp. 359\u2013370. IEEE Compute Society (2011). https:\/\/doi.org\/10.1109\/DSN.2011.5958249","DOI":"10.1109\/DSN.2011.5958249"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-39634-2_9","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2013","unstructured":"Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 84\u201399. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_9"},{"key":"13_CR21","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":"13_CR22","doi-asserted-by":"crossref","unstructured":"Lothaire, M.: Algebraic Combinatorics on Words, Encyclopedia of Mathematics and its Applications. Cambridge University Press (2002)","DOI":"10.1017\/CBO9781107326019"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-38613-8_12","volume-title":"Integrated Formal Methods","author":"S Song","year":"2013","unstructured":"Song, S., Gui, L., Sun, J., Liu, Y., Dong, J.S.: Improved reachability analysis in DTMC via divide and conquer. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 162\u2013176. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38613-8_12"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Tao, T.: An Introduction to Measure Theory. American Mathematical Society (2011)","DOI":"10.1090\/gsm\/126"},{"key":"13_CR25","unstructured":"The PARI\u00a0Group, Univ. Bordeaux: PARI\/GP version 2.11.0 (2018). http:\/\/pari.math.u-bordeaux.fr\/"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-09524-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T21:14:09Z","timestamp":1762290849000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-09524-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,5]]},"ISBN":["9783032095237","9783032095244"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-09524-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,5]]},"assertion":[{"value":"5 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"An extended version of this paper, which includes an appendix with the full proofs as well as the code shown in Listing\u00a01 in a separate file, is available on arXiv with DOI\n                      \n                      \u00a0[\n                      \n                      ].","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Extended Version and Data Availability"}},{"value":"RP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Reachability Problems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Madrid","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","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":"1 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rp2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rp25.software.imdea.org\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}