{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T16:07:52Z","timestamp":1779034072613,"version":"3.51.4"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Practical verification tasks often involve multiple goals, such as maximising an expected reward within a specified reliability threshold. Algorithms to solve such multi-objective probabilistic model checking (MO-PMC) problems were developed over a decade ago, and are implemented by multiple tools. However, the algorithms are\n                    <jats:italic>unsound<\/jats:italic>\n                    in general\u2014at best delivering some underapproximation of the true result\u2014and the implementations are unreliable, with different tools producing inconsistent results. In this paper, we present the first implementations of recently-developed\n                    <jats:italic>sound<\/jats:italic>\n                    MO-PMC algorithms that bound the true result from above\n                    <jats:italic>and<\/jats:italic>\n                    below, in two independent tools. We discuss ways to consistently treat infinite rewards and extend the algorithms with relative-error termination criteria. On the practical side, we add support for multi-objective properties to the\n                    <jats:sc>Jani<\/jats:sc>\n                    interchange format for tool interoperability, and extend the Quantitative Verification Benchmark Set with multi-objective problems. Based on the latter, we conduct an extensive experimental evaluation of the two tools\u2019 new sound MO-PMC capabilities, showing in particular that they produce consistent results.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_10","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:49:53Z","timestamp":1779032993000},"page":"189-210","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Tools and\u00a0Algorithms for\u00a0Sound Multi-Objective Probabilistic Model Checking"],"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-0002-2843-5511","authenticated-orcid":false,"given":"Tim","family":"Quatmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-8239-3164","authenticated-orcid":false,"given":"Mark","family":"van Wijk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","unstructured":"Andriushchenko, R., et al.: Tools at the frontiers of quantitative verification \u2013 QComp 2023 competition report. In: Beyer, D., Hartmanns, A., Kordon, F. (eds.) TOOLympics Challenge 2023 \u2013 Updates, Results, Successes of the Formal-Methods Competitions (TOOLympics 2023). Lecture Notes in Computer Science, vol. 14550, pp. 90\u2013146. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-67695-6_4","DOI":"10.1007\/978-3-031-67695-6_4"},{"key":"10_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":"10_CR3","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2024.105214","volume":"301","author":"C Baier","year":"2024","unstructured":"Baier, C., Chatterjee, K., Meggendorfer, T., Piribauer, J.: Entropic risk for turn-based stochastic games. Inf. Comput. 301, 105214 (2024). https:\/\/doi.org\/10.1016\/J.IC.2024.105214","journal-title":"Inf. Comput."},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Baier, C., Chau, C., Drobitko, V., Jantsch, S., Kl\u00fcppelholz, S.: Certificates and witnesses for multi-objective \u00f8mega-regular queries in Markov decision processes. In: Bianculli, D., G\u00f3mez-Mart\u00ednez, E. (eds.) Software Engineering and Formal Methods - 23rd International Conference, SEFM 2025, Toledo, Spain, November 10-14, 2025, Proceedings. Lecture Notes in Computer Science, vol. 16192, pp. 129\u2013147. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-032-10444-1_8","DOI":"10.1007\/978-3-032-10444-1_8"},{"key":"10_CR5","doi-asserted-by":"publisher","DOI":"10.1016\/J.PEVA.2025.102482","volume":"168","author":"C Baier","year":"2025","unstructured":"Baier, C., Chau, C., Kl\u00fcppelholz, S.: Certificates and witnesses for multi-objective queries in Markov decision processes. Perform. Eval. 168, 102482 (2025). https:\/\/doi.org\/10.1016\/J.PEVA.2025.102482","journal-title":"Perform. Eval."},{"key":"10_CR6","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-63387-9_8","volume-title":"Computer Aided Verification","author":"C Baier","year":"2017","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the Reliability of Your Model Checker: interval iteration for Markov decision processes. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 160\u2013180. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8"},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"Bals, S., Evangelidis, A., Kret\u00ednsk\u00fd, J., Waibel, J.: MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints. In: \u00c1brah\u00e1m, E., Jr., M.M. (eds.) Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024, Hong Kong SAR, China, May 14-16, 2024, pp. 24:1\u201324:7. ACM (2024). https:\/\/doi.org\/10.1145\/3641513.3650135","DOI":"10.1145\/3641513.3650135"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Basset, N., Kwiatkowska, M.Z., Topcu, U., Wiltsche, C.: Strategy synthesis for stochastic games with multiple long-run objectives. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science, vol.\u00a09035, pp. 256\u2013271. Springer, Berlin, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_22","DOI":"10.1007\/978-3-662-46681-0_22"},{"issue":"5","key":"10_CR10","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."},{"issue":"2","key":"10_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."},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-662-46681-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Br\u00e1zdil","year":"2015","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Forejt, V., Ku\u010dera, A.: MultiGain: a controller synthesis tool for MDPs with multiple mean-payoff objectives. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 181\u2013187. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_12"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Chatterjee, K., Forejt, V., Ku\u010dera, A.: Markov decision processes with multiple long-run average objectives. Log. Methods Comput. Sci. 10(1) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(1:13)2014","DOI":"10.2168\/LMCS-10(1:13)2014"},{"key":"10_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: Legay, A., Margaria, T. (eds.) 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017). 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"},{"issue":"1","key":"10_CR15","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/S10703-023-00411-4","volume":"63","author":"K Chatterjee","year":"2024","unstructured":"Chatterjee, K., Katoen, J., Mohr, S., Weininger, M., Winkler, T.: Stochastic games with lexicographic objectives. Formal Methods Syst. Des. 63(1), 40\u201380 (2024). https:\/\/doi.org\/10.1007\/S10703-023-00411-4","journal-title":"Formal Methods Syst. Des."},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19835-9_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 112\u2013127. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33386-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"V Forejt","year":"2012","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 317\u2013332. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_25"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-030-94583-1_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C Fu","year":"2022","unstructured":"Fu, C., Hahn, E.M., Li, Y., Schewe, S., Sun, M., Turrini, A., Zhang, L.: EPMC gets knowledge in multi-agent systems. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 93\u2013107. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_5"},{"key":"10_CR19","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":"10_CR20","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":"5","key":"10_CR21","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994). https:\/\/doi.org\/10.1007\/BF01211866","journal-title":"Formal Aspects Comput."},{"key":"10_CR22","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":"10_CR23","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"},{"issue":"7","key":"10_CR24","doi-asserted-by":"publisher","first-page":"1483","DOI":"10.1007\/S10817-020-09574-9","volume":"64","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Junges, S., Katoen, J., Quatmann, T.: Multi-cost bounded tradeoff analysis in MDP. J. Autom. Reason. 64(7), 1483\u20131522 (2020). https:\/\/doi.org\/10.1007\/S10817-020-09574-9","journal-title":"J. Autom. Reason."},{"key":"10_CR25","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, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_24","DOI":"10.1007\/978-3-031-30823-9_24"},{"key":"10_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":"10_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":"10_CR28","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Quatmann, T., van Wijk, M.: Tools and algorithms for sound multi-objective probabilistic model checking (artifact) (2026). https:\/\/doi.org\/10.5281\/zenodo.18604533","DOI":"10.5281\/zenodo.18604533"},{"key":"10_CR29","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2023.102987","volume":"230","author":"IR Hasrat","year":"2023","unstructured":"Hasrat, I.R., Jensen, P.G., Larsen, K.G., Srba, J.: A toolchain for domestic heat-pump control using Uppaal Stratego. Sci. Comput. Program. 230, 102987 (2023). https:\/\/doi.org\/10.1016\/J.SCICO.2023.102987","journal-title":"Sci. Comput. Program."},{"key":"10_CR30","unstructured":"Hausdorff, F.: Grundz\u00fcge der Mengenlehre (1914)"},{"issue":"4","key":"10_CR31","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":"10_CR32","volume-title":"Dynamic Programming and Markov Processes","author":"RA Howard","year":"1960","unstructured":"Howard, R.A.: Dynamic Programming and Markov Processes. MIT Press, Cambridge (1960)"},{"key":"10_CR33","doi-asserted-by":"publisher","unstructured":"Hwang, C.L., Masud, A.S.M.: Multiple Objective Decision Making \u2013 Methods and Applications. Lecture Notes in Economics and Mathematical Systems, Springer, Berlin, Heidelberg (1979). https:\/\/doi.org\/10.1007\/978-3-642-45511-7","DOI":"10.1007\/978-3-642-45511-7"},{"key":"10_CR34","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). Lecture Notes in Computer Science, vol. 15932, pp. 122\u2013146. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98679-6_6","DOI":"10.1007\/978-3-031-98679-6_6"},{"key":"10_CR35","doi-asserted-by":"publisher","unstructured":"Kr\u00e4hmann, D., Schubert, J., Baier, C., Dubslaff, C.: Ratio and weight quantiles. In: Italiano, G.F., Pighizzini, G., Sannella, D. (eds.) 40th International Symposium on Mathematical Foundations of Computer Science 2015 (MFCS). Lecture Notes in Computer Science, vol.\u00a09234, pp. 344\u2013356. Springer, Berlin, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48057-1_27","DOI":"10.1007\/978-3-662-48057-1_27"},{"key":"10_CR36","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J.: LTL-constrained steady-state policy synthesis. In: Zhou, Z. (ed.) 30th International Joint Conference on Artificial Intelligence (IJCAI 2021), pp. 4104\u20134111. ijcai.org (2021). https:\/\/doi.org\/10.24963\/IJCAI.2021\/565","DOI":"10.24963\/IJCAI.2021\/565"},{"key":"10_CR37","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Conditional value-at-risk for reachability and mean payoff in Markov decision processes. In: Dawar, A., Gr\u00e4del, E. (eds.) 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 609\u2013618. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209176","DOI":"10.1145\/3209108.3209176"},{"key":"10_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-030-53291-8_25","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2020","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 475\u2013487. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_25"},{"key":"10_CR39","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"},{"key":"10_CR40","doi-asserted-by":"publisher","unstructured":"Moffaert, K.V., Drugan, M.M., Now\u00e9, A.: Scalarized multi-objective reinforcement learning: novel design techniques. In: 2013 IEEE Symposium on Adaptive Dynamic Programming and Reinforcement Learning (ADPRL 2013), pp. 191\u2013199. IEEE (2013). https:\/\/doi.org\/10.1109\/ADPRL.2013.6615007","DOI":"10.1109\/ADPRL.2013.6615007"},{"key":"10_CR41","doi-asserted-by":"publisher","unstructured":"Quatmann, T.: Verification of multi-objective Markov models. Ph.D. thesis, RWTH Aachen University (2023). https:\/\/doi.org\/10.18154\/RWTH-2023-09669","DOI":"10.18154\/RWTH-2023-09669"},{"issue":"1","key":"10_CR42","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/S10703-021-00364-6","volume":"60","author":"T Quatmann","year":"2022","unstructured":"Quatmann, T., Junges, S., Katoen, J.: Markov automata with multiple objectives. Formal Methods Syst. Des. 60(1), 33\u201386 (2022). https:\/\/doi.org\/10.1007\/S10703-021-00364-6","journal-title":"Formal Methods Syst. Des."},{"key":"10_CR43","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":"10_CR44","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.P.: Multi-objective optimization of long-run average and total rewards. In: Groote, J.F., Larsen, K.G. (eds.) 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021). Lecture Notes in Computer Science, vol. 12651, pp. 230\u2013249. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_13","DOI":"10.1007\/978-3-030-72016-2_13"},{"issue":"10","key":"10_CR45","doi-asserted-by":"publisher","first-page":"1095","DOI":"10.1073\/pnas.39.10.1095","volume":"39","author":"L Shapley","year":"1953","unstructured":"Shapley, L.: Stochastic games. Proc. Natl. Acad. Sci. U.S.A. 39(10), 1095\u20131100 (1953). https:\/\/doi.org\/10.1073\/pnas.39.10.1095","journal-title":"Proc. Natl. Acad. Sci. U.S.A."},{"key":"10_CR46","unstructured":"Simaitis, A.: Automatic verification of competitive stochastic systems. Ph.D. thesis, University of Oxford, UK (2014). http:\/\/ora.ox.ac.uk\/objects\/uuid:68b5e2d8-ba04-419f-8926-4cd542121e2d"},{"key":"10_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-37075-5_23","volume-title":"Foundations of Software Science and Computation Structures","author":"M Ummels","year":"2013","unstructured":"Ummels, M., Baier, C.: Computing quantiles in Markov reward models. In: Pfenning, F. (ed.) FoSSaCS 2013. LNCS, vol. 7794, pp. 353\u2013368. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37075-5_23"},{"key":"10_CR48","doi-asserted-by":"publisher","unstructured":"Watanabe, K., van\u00a0der Vegt, M., Hasuo, I., Rot, J., Junges, S.: Pareto curves for compositionally model checking string diagrams of MDPs. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024). Lecture Notes in Computer Science, vol. 14571, pp. 279\u2013298. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57249-4_14","DOI":"10.1007\/978-3-031-57249-4_14"},{"key":"10_CR49","unstructured":"van Wijk, M.: The State of Multi-objective Model Checking. Master\u2019s thesis, University of Twente (2024). https:\/\/purl.utwente.nl\/essays\/104622"},{"key":"10_CR50","doi-asserted-by":"publisher","unstructured":"Wray, K.H., Zilberstein, S., Mouaddib, A.: Multi-objective MDPs with conditional lexicographic reward preferences. In: Bonet, B., Koenig, S. (eds.) Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA, pp. 3418\u20133424. AAAI Press (2015). https:\/\/doi.org\/10.1609\/AAAI.V29I1.9647","DOI":"10.1609\/AAAI.V29I1.9647"}],"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-032-26204-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:49:55Z","timestamp":1779032995000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_10"}},"subtitle":["(Long Tool Paper)"],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","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":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}