{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T12:40:12Z","timestamp":1756298412303,"version":"3.44.0"},"publisher-location":"Cham","reference-count":68,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032009418","type":"print"},{"value":"9783032009425","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T00:00:00Z","timestamp":1756339200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T00:00:00Z","timestamp":1756339200000},"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-00942-5_2","type":"book-chapter","created":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T12:03:29Z","timestamp":1756296209000},"page":"21-36","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Overview of\u00a0Sound and\u00a0Modest Approaches to\u00a0Quantitative Model Checking from\u00a0Sea to\u00a0Space"],"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"}]}],"member":"297","published-online":{"date-parts":[[2025,8,28]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018). https:\/\/doi.org\/10.1145\/3158668","DOI":"10.1145\/3158668"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Alfaro","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 395\u2013410. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46419-0_27"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-030-72013-1_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Ashok","year":"2021","unstructured":"Ashok, P., Jackermeier, M., K\u0159et\u00ednsk\u00fd, J., Weinhuber, C., Weininger, M., Yadav, M.: dtControl 2.0: explainable strategy representation via decision tree learning steered by experts. In: TACAS 2021. LNCS, vol. 12652, pp. 326\u2013345. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_17"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Baier, C.: Probabilistic model checking. In: Esparza, J., Grumberg, O., Sickert, S. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series \u2013 D: Information and Communication Security, vol.\u00a045, pp. 1\u201323. IOS Press (2016). https:\/\/doi.org\/10.3233\/978-1-61499-627-9-1","DOI":"10.3233\/978-1-61499-627-9-1"},{"key":"2_CR5","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: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"issue":"9","key":"2_CR6","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C Baier","year":"2010","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76\u201385 (2010). https:\/\/doi.org\/10.1145\/1810891.1810912","journal-title":"Commun. ACM"},{"key":"2_CR7","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Balbo, G.: Introduction to generalized stochastic Petri nets. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 83\u2013131. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72522-0_3","DOI":"10.1007\/978-3-540-72522-0_3"},{"issue":"5","key":"2_CR9","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":"2_CR10","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-031-90660-2_9","volume-title":"TACAS 2025","author":"D Beyer","year":"2025","unstructured":"Beyer, D., Strejcek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: Gurfinkel, A., Heule, M. (eds.) TACAS 2025. LNCS, vol. 15698, pp. 151\u2013186. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-90660-2_9"},{"issue":"2","key":"2_CR11","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/S00165-018-0458-2","volume":"31","author":"M Bisgaard","year":"2019","unstructured":"Bisgaard, M., Gerhardt, D., Hermanns, H., Krc\u00e1l, J., Nies, G., Stenger, M.: Battery-aware scheduling in low orbit: the GomX-3 case. Formal Aspects Comput. 31(2), 261\u2013285 (2019). https:\/\/doi.org\/10.1007\/S00165-018-0458-2","journal-title":"Formal Aspects Comput."},{"issue":"10","key":"2_CR12","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.P.: MoDeST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng. 32(10), 812\u2013830 (2006). https:\/\/doi.org\/10.1109\/TSE.2006.104","journal-title":"IEEE Trans. Software Eng."},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-45232-4_8","volume-title":"Computer Performance Evaluation. Modelling Techniques and Tools","author":"H Bohnenkamp","year":"2003","unstructured":"Bohnenkamp, H., Hermanns, H., Katoen, J.-P., Klaren, R.: The Modest modeling tool and its implementation. In: Kemper, P., Sanders, W.H. (eds.) TOOLS 2003. LNCS, vol. 2794, pp. 116\u2013133. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45232-4_8"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Bohnenkamp, H.C., Hermanns, H., Klaren, R., Mader, A., Usenko, Y.S.: Synthesis and stochastic assessment of schedules for lacquer production. In: 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), pp. 28\u201337. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/QEST.2004.1348013","DOI":"10.1109\/QEST.2004.1348013"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Fraire, J.A., Hartmanns, A., Zhang, Z.: Modest models and tools for real stochastic timed systems. In: Jansen, N., et al. (eds.) Principles of Verification: Cycling the Probabilistic Landscape \u2013 Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 15261, pp. 115\u2013142. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-75775-4_6","DOI":"10.1007\/978-3-031-75775-4_6"},{"key":"2_CR16","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/J.SCICO.2019.01.006","volume":"174","author":"CE Budde","year":"2019","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A.: Automated compositional importance splitting. Sci. Comput. Program. 174, 90\u2013108 (2019). https:\/\/doi.org\/10.1016\/J.SCICO.2019.01.006","journal-title":"Sci. Comput. Program."},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A.: Digging for decision trees: a case study in strategy sampling and learning. In: Steffen, B. (ed.) 2nd International Conference on Bridging the Gap Between AI and Reality (AISoLA 2024). Lecture Notes in Computer Science, vol. 15217, pp. 354\u2013378. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-75434-0_24","DOI":"10.1007\/978-3-031-75434-0_24"},{"issue":"6","key":"2_CR18","doi-asserted-by":"publisher","first-page":"759","DOI":"10.1007\/S10009-020-00563-2","volume":"22","author":"CE Budde","year":"2020","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: An efficient statistical model checker for nondeterminism and rare events. Int. J. Softw. Tools Technol. Transf. 22(6), 759\u2013780 (2020). https:\/\/doi.org\/10.1007\/S10009-020-00563-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-662-54580-5_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2017","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 151\u2013168. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9"},{"key":"2_CR20","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":"2_CR21","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Hartmanns, A., Meggendorfer, T., Weininger, M., Wienh\u00f6ft, P.: Sound statistical model checking for probabilities and expected rewards. In: Gurfinkel, A., Heule, M. (eds.) 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025). Lecture Notes in Computer Science, vol. 15696, pp. 167\u2013190. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90643-5_9","DOI":"10.1007\/978-3-031-90643-5_9"},{"key":"2_CR22","unstructured":"Budde, C.E., Hartmanns, A., Meggendorfer, T., Weininger, M., Wienh\u00f6ft, P.: Statistical model checking beyond means: Quantiles, CVaR, and the DKW inequality. In: 2nd International Joint Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems (QEST-FORMATS 2025). Lecture Notes in Computer Science, vol. 16143. Springer (2025)"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Butkova, Y., Hartmanns, A., Hermanns, H.: A Modest approach to Markov automata. ACM Trans. Model. Comput. Simul. 31(3), 14:1\u201314:34 (2021). https:\/\/doi.org\/10.1145\/3449355","DOI":"10.1145\/3449355"},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Quatmann, T., Sch\u00e4ffeler, M., Weininger, M., Winkler, T., Zilken, D.: Fixed point certificates for reachability and expected rewards in MDPs. In: Gurfinkel, A., Heule, M. (eds.) 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025). Lecture Notes in Computer Science, vol. 15697, pp. 130\u2013151. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90653-4_7","DOI":"10.1007\/978-3-031-90653-4_7"},{"issue":"4","key":"2_CR25","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1093\/biomet\/26.4.404","volume":"26","author":"C Clopper","year":"1934","unstructured":"Clopper, C., Pearson, E.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26(4), 404\u2013413 (1934). https:\/\/doi.org\/10.1093\/biomet\/26.4.404","journal-title":"Biometrika"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-030-55754-6_17","volume-title":"NASA Formal Methods","author":"PR D\u2019Argenio","year":"2020","unstructured":"D\u2019Argenio, P.R., Fraire, J.A., Hartmanns, A.: Sampling distributed schedulers for\u00a0resilient space communication. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 291\u2013310. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_17"},{"key":"2_CR27","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Fraire, J.A., Hartmanns, A., Raverta, F.D.: Comparing statistical, analytical, and learning-based routing approaches for delay-tolerant networks. ACM Trans. Model. Comput. Simul. 35(2), 10:1\u201310:26 (2025). https:\/\/doi.org\/10.1145\/3665927","DOI":"10.1145\/3665927"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-33693-0_7","volume-title":"Integrated Formal Methods","author":"PR D\u2019Argenio","year":"2016","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Legay, A., Sedwards, S.: Statistical approximation of optimal schedulers for probabilistic timed automata. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 99\u2013114. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_7"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-030-03421-4_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"PR D\u2019Argenio","year":"2018","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: Lightweight statistical model checking in nondeterministic continuous time. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 336\u2013353. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_22"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45605-8_5","volume-title":"Process Algebra and Probabilistic Methods: Performance Modeling and Verification","author":"PR D\u2019Argenio","year":"2002","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and refinement strategies for probabilistic analysis. In: Hermanns, H., Segala, R. (eds.) PAPM-PROBMIV 2002. LNCS, vol. 2399, pp. 57\u201376. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45605-8_5"},{"issue":"4","key":"2_CR31","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.M.: Smart sampling for lightweight verification of Markov decision processes. Int. J. Softw. Tools Technol. Transf. 17(4), 469\u2013484 (2015). https:\/\/doi.org\/10.1007\/S10009-015-0383-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"2_CR32","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1214\/aoms\/1177728174","volume":"27","author":"A Dvoretzky","year":"1956","unstructured":"Dvoretzky, A., Kiefer, J., Wolfowitz, J.: Asymptotic minimax character of the sample distribution function and of the classical multinomial estimator. Ann. Math. Stat. 27(3), 642\u2013669 (1956). https:\/\/doi.org\/10.1214\/aoms\/1177728174","journal-title":"Ann. Math. Stat."},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010), pp. 342\u2013351. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/LICS.2010.41","DOI":"10.1109\/LICS.2010.41"},{"key":"2_CR34","doi-asserted-by":"publisher","unstructured":"Fr\u00e4nzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: Caccamo, M., Frazzoli, E., Grosu, R. (eds.) 14th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2011), pp. 43\u201352. ACM (2011). https:\/\/doi.org\/10.1145\/1967701.1967710","DOI":"10.1145\/1967701.1967710"},{"issue":"3","key":"2_CR35","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/S10009-007-0062-X","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10(3), 263\u2013279 (2008). https:\/\/doi.org\/10.1007\/S10009-007-0062-X","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-540-75454-1_14","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Giro","year":"2007","unstructured":"Giro, S., D\u2019Argenio, P.R.: Quantitative model checking revisited: neither decidable nor approximable. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 179\u2013194. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_14"},{"key":"2_CR37","doi-asserted-by":"publisher","unstructured":"Gribaudo, M., Remke, A.: Hybrid Petri nets with general one-shot transitions for dependability evaluation of fluid critical infrastructures. In: 12th IEEE High Assurance Systems Engineering Symposium (HASE 2010), pp. 84\u201393. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/HASE.2010.27","DOI":"10.1109\/HASE.2010.27"},{"key":"2_CR38","unstructured":"G\u00f6teborgs stad, H\u00e4rryda kommun, M\u00f6lndals stad: M\u00f6lndals\u00e5n \u2013 reglerad livsnerv genom tre kommuner. https:\/\/molndalsan.se\/molndalsan.pdf. Accessed 06 June 2025"},{"key":"2_CR39","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":"2_CR40","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."},{"issue":"2","key":"2_CR41","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/S10703-012-0167-Z","volume":"43","author":"EM Hahn","year":"2013","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013). https:\/\/doi.org\/10.1007\/S10703-012-0167-Z","journal-title":"Formal Methods Syst. Des."},{"key":"2_CR42","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: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13244, pp. 41\u201359. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_3"},{"key":"2_CR43","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":"2_CR44","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/J.SCICO.2015.08.009","volume":"112","author":"A Hartmanns","year":"2015","unstructured":"Hartmanns, A., Hermanns, H.: In the quantitative automata zoo. Sci. Comput. Program. 112, 3\u201323 (2015). https:\/\/doi.org\/10.1016\/J.SCICO.2015.08.009","journal-title":"Sci. Comput. Program."},{"key":"2_CR45","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: A Modest Markov automata tutorial. In: Kr\u00f6tzsch, M., Stepanova, D. (eds.) Reasoning Web. Explainable Artificial Intelligence. LNCS, vol. 11810, pp. 250\u2013276. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31423-1_8","DOI":"10.1007\/978-3-030-31423-1_8"},{"key":"2_CR46","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner\u2019s guide to MDP model checking algorithms. In: Sankaranarayanan, S., Sharygina, N. (eds.) 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023). 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":"2_CR47","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":"2_CR48","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). Lecture Notes in Computer Science, 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":"2_CR49","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Sedwards, S., D\u2019Argenio, P.R.: Efficient simulation-based verification of probabilistic timed automata. In: 2017 Winter Simulation Conference (WSC 2017), pp. 1419\u20131430. IEEE (2017). https:\/\/doi.org\/10.1109\/WSC.2017.8247885","DOI":"10.1109\/WSC.2017.8247885"},{"key":"2_CR50","unstructured":"Hatefi-Ardakani, H.: Finite horizon analysis of Markov automata. Ph.D. thesis, Saarland University, Germany (2017). http:\/\/scidok.sulb.uni-saarland.de\/volltexte\/2017\/6743\/"},{"issue":"4","key":"2_CR51","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":"2_CR52","unstructured":"Howard, R.A.: Dynamic Programming and Markov Processes. MIT Press (1960)"},{"key":"2_CR53","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: 37th International Conference on Computer Aided Verification (CAV 2025). Lecture Notes in Computer Science. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98679-6_6","DOI":"10.1007\/978-3-031-98679-6_6"},{"key":"2_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"2_CR55","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/S10703-006-0005-2","volume":"29","author":"MZ Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: 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","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"2_CR56","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":"2_CR57","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":"2_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-319-15201-1_23","volume-title":"Software Engineering and Formal Methods","author":"A Legay","year":"2015","unstructured":"Legay, A., Sedwards, S., Traonouez, L.-M.: Scalable verification of Markov decision processes. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 350\u2013362. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15201-1_23"},{"issue":"3","key":"2_CR59","doi-asserted-by":"publisher","first-page":"1269","DOI":"10.1214\/aop\/1176990746","volume":"18","author":"P Massart","year":"1990","unstructured":"Massart, P.: The tight constant in the Dvoretzky-Kiefer-Wolfowitz inequality. Ann. Probab. 18(3), 1269\u20131283 (1990). https:\/\/doi.org\/10.1214\/aop\/1176990746","journal-title":"Ann. Probab."},{"key":"2_CR60","doi-asserted-by":"publisher","unstructured":"Niehage, M., Hartmanns, A., Remke, A.: Learning optimal decisions for stochastic hybrid systems. In: Arun-Kumar, S., M\u00e9ry, D., Saha, I., Zhang, L. (eds.) 19th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2021), pp. 44\u201355. ACM (2021). https:\/\/doi.org\/10.1145\/3487212.3487339","DOI":"10.1145\/3487212.3487339"},{"key":"2_CR61","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 a proof assistant for Higher-Order Logic. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"2_CR62","doi-asserted-by":"publisher","unstructured":"Oliehoek, F.A., Amato, C.: A Concise Introduction to Decentralized POMDPs. Springer Briefs in Intelligent Systems. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-28929-8","DOI":"10.1007\/978-3-319-28929-8"},{"key":"2_CR63","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":"2_CR64","doi-asserted-by":"publisher","DOI":"10.1016\/j.adhoc.2021.102663","volume":"123","author":"FD Raverta","year":"2021","unstructured":"Raverta, F.D., Fraire, J.A., Madoery, P.G., Demasi, R.A., Finochietto, J.M., D\u2019Argenio, P.R.: Routing in delay-tolerant networks under uncertain contact plans. Ad Hoc Netw. 123, 102663 (2021). https:\/\/doi.org\/10.1016\/j.adhoc.2021.102663","journal-title":"Ad Hoc Netw."},{"key":"2_CR65","doi-asserted-by":"publisher","unstructured":"Rubino, G., Tuffin, B. (eds.): Rare Event Simulation using Monte Carlo Methods. Wiley (2009). https:\/\/doi.org\/10.1002\/9780470745403","DOI":"10.1002\/9780470745403"},{"key":"2_CR66","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning - An Introduction. Adaptive Computation and Machine Learning. MIT Press (1998)"},{"key":"2_CR67","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/BF00992698","volume":"8","author":"CJCH Watkins","year":"1992","unstructured":"Watkins, C.J.C.H., Dayan, P.: Q-learning. Mach. Learn. 8, 279\u2013292 (1992). https:\/\/doi.org\/10.1007\/BF00992698","journal-title":"Mach. Learn."},{"key":"2_CR68","doi-asserted-by":"publisher","unstructured":"Wimmer, R., Kortus, A., Herbstritt, M., Becker, B.: Probabilistic model checking and reliability of results. In: Straube, B., Drutarovsk\u00fd, M., Renovell, M., Gramata, P., Fischerov\u00e1, M. (eds.) 11th IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS 2008), pp. 207\u2013212. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/DDECS.2008.4538787","DOI":"10.1109\/DDECS.2008.4538787"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-00942-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T12:03:34Z","timestamp":1756296214000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-00942-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,28]]},"ISBN":["9783032009418","9783032009425"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-00942-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,28]]},"assertion":[{"value":"28 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aarhus","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","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":"27 August 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 August 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fmics2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/FMICS2025.uni-muenster.de","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}