{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:49:43Z","timestamp":1782877783911,"version":"3.54.5"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227515","type":"print"},{"value":"9783032227522","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-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T00:00:00Z","timestamp":1776297600000},"content-version":"vor","delay-in-days":105,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22752-2_27","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T21:51:50Z","timestamp":1776289910000},"page":"526-546","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Multiple Long-Run and $$\\omega $$-Regular Objectives in MDPs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-5755-1193","authenticated-orcid":false,"given":"Julius","family":"Ide","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-6815-3285","authenticated-orcid":false,"given":"Hannah","family":"Mertens","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2843-5511","authenticated-orcid":false,"given":"Tim","family":"Quatmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,16]]},"reference":[{"key":"27_CR1","doi-asserted-by":"publisher","unstructured":"Andriushchenko, R., Bork, A., Budde, C.E., Ceska, M., Grover, K., 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: TOOLympics@ETAPS. Lecture Notes in Computer Science, vol. 14550, pp. 90\u2013146. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-67695-6_4","DOI":"10.1007\/978-3-031-67695-6_4"},{"key":"27_CR2","doi-asserted-by":"publisher","unstructured":"Ashok, P., Chatterjee, K., Daca, P., Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Value iteration for long-run average reward in Markov decision processes. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10426, pp. 201\u2013221. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_10","DOI":"10.1007\/978-3-319-63387-9_10"},{"key":"27_CR3","doi-asserted-by":"publisher","unstructured":"Baier, C., Chau, C., Kl\u00fcppelholz, S.: Certificates and witnesses for multi-objective queries in Markov decision processes. Perform. Evaluation 168, 102482 (2025). https:\/\/doi.org\/10.1016\/J.PEVA.2025.102482","DOI":"10.1016\/J.PEVA.2025.102482"},{"key":"27_CR4","unstructured":"Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)"},{"key":"27_CR5","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":"27_CR6","doi-asserted-by":"publisher","unstructured":"Barrett, L., Narayanan, S.: Learning all optimal policies with multiple criteria. In: ICML. ACM International Conference Proceeding Series, vol.\u00a0307, pp. 41\u201347. ACM (2008). https:\/\/doi.org\/10.1145\/1390156.1390162","DOI":"10.1145\/1390156.1390162"},{"key":"27_CR7","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, 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":"27_CR8","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Forejt, V., Kucera, A.: MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. In: TACAS. Lecture Notes in Computer Science, vol.\u00a09035, pp. 181\u2013187. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_12","DOI":"10.1007\/978-3-662-46681-0_12"},{"key":"27_CR9","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":"27_CR10","doi-asserted-by":"publisher","unstructured":"Butkova, Y., Wimmer, R., Hermanns, H.: Long-run rewards for Markov automata. In: TACAS (2). Lecture Notes in Computer Science, vol. 10206, pp. 188\u2013203 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_11","DOI":"10.1007\/978-3-662-54580-5_11"},{"key":"27_CR11","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Kret\u00ednsk\u00e1, Z., Kret\u00ednsk\u00fd, J.: Unifying two views on multiple mean-payoff objectives in Markov decision processes. Log. Methods Comput. Sci. 13(2) (2017). https:\/\/doi.org\/10.23638\/LMCS-13(2:15)2017","DOI":"10.23638\/LMCS-13(2:15)2017"},{"key":"27_CR12","doi-asserted-by":"publisher","unstructured":"Chen, T., Kwiatkowska, M.Z., Simaitis, A., Wiltsche, C.: Synthesis for multi-objective stochastic games: An application to autonomous urban driving. In: Joshi, K.R., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a08054, pp. 322\u2013337. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-40196-1_28","DOI":"10.1007\/978-3-642-40196-1_28"},{"key":"27_CR13","doi-asserted-by":"publisher","unstructured":"Chen, Y., Tumova, J., Belta, C.: LTL robot motion control based on automata learning of environmental dynamics. In: IEEE International Conference on Robotics and Automation, ICRA 2012, 14-18 May, 2012, St. Paul, Minnesota, USA. pp. 5177\u20135182. IEEE (2012). https:\/\/doi.org\/10.1109\/ICRA.2012.6225075","DOI":"10.1109\/ICRA.2012.6225075"},{"key":"27_CR14","doi-asserted-by":"publisher","unstructured":"Ding, X.C., Smith, S.L., Belta, C., Rus, D.: MDP optimal control under temporal logic constraints. In: 50th IEEE Conference on Decision and Control and European Control Conference, 11th European Control Conference, CDC\/ECC 2011, Orlando, FL, USA, December 12-15, 2011. pp. 532\u2013538. IEEE (2011). https:\/\/doi.org\/10.1109\/CDC.2011.6161122","DOI":"10.1109\/CDC.2011.6161122"},{"key":"27_CR15","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Renault, E., Colange, M., Renkin, F., Aisse, A.G., Schlehuber-Caissier, P., Medioni, T., Martin, A., Dubois, J., Gillard, C., Lauko, H.: From spot 2.0 to spot 2.10: What\u2019s new? In: CAV (2). Lecture Notes in Computer Science, vol. 13372, pp. 174\u2013187. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"27_CR16","doi-asserted-by":"publisher","unstructured":"Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci. 4(4) (2008). https:\/\/doi.org\/10.2168\/LMCS-4(4:8)2008","DOI":"10.2168\/LMCS-4(4:8)2008"},{"key":"27_CR17","doi-asserted-by":"publisher","unstructured":"Feng, L., Kwiatkowska, M.Z., Parker, D.: Automated learning of probabilistic assumptions for compositional reasoning. In: FASE. Lecture Notes in Computer Science, vol.\u00a06603, pp. 2\u201317. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19811-3_2","DOI":"10.1007\/978-3-642-19811-3_2"},{"key":"27_CR18","doi-asserted-by":"publisher","unstructured":"Feng, L., Wiltsche, C., Humphrey, L.R., Topcu, U.: Controller synthesis for autonomous systems interacting with human operators. In: ICCPS. pp. 70\u201379. ACM (2015). https:\/\/doi.org\/10.1145\/2735960.2735973","DOI":"10.1145\/2735960.2735973"},{"key":"27_CR19","doi-asserted-by":"publisher","unstructured":"Filar, J.A., Krass, D., Ross, K.: Percentile performance criteria for limiting average Markov decision processes. IEEE Trans. Autom. Control. 40(1), 2\u201310 (1995). https:\/\/doi.org\/10.1109\/9.362904","DOI":"10.1109\/9.362904"},{"key":"27_CR20","doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06605, pp. 112\u2013127. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11","DOI":"10.1007\/978-3-642-19835-9_11"},{"key":"27_CR21","doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M.Z., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07561, pp. 317\u2013332. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_25","DOI":"10.1007\/978-3-642-33386-6_25"},{"key":"27_CR22","doi-asserted-by":"publisher","unstructured":"Guo, M., Zavlanos, M.M.: Probabilistic motion planning under temporal tasks and soft constraints. IEEE Trans. Autom. Control. 63(12), 4051\u20134066 (2018). https:\/\/doi.org\/10.1109\/TAC.2018.2799561","DOI":"10.1109\/TAC.2018.2799561"},{"key":"27_CR23","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2025), https:\/\/www.gurobi.com"},{"key":"27_CR24","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":"27_CR25","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":"27_CR26","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/S10009-021-00633-Z","DOI":"10.1007\/S10009-021-00633-Z"},{"key":"27_CR27","doi-asserted-by":"publisher","unstructured":"Ide, J., Katoen, J.P., Mertens, H., Quatmann, T.: Artifact for paper: Multiple long-run and omega-regular objectives in MDPs. Zenodo (2026). https:\/\/doi.org\/10.5281\/zenodo.18194069","DOI":"10.5281\/zenodo.18194069"},{"key":"27_CR28","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Pasareanu, C.S., Clarke, E.M.: Assume-guarantee abstraction refinement for probabilistic systems. In: CAV. Lecture Notes in Computer Science, vol.\u00a07358, pp. 310\u2013326. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_25","DOI":"10.1007\/978-3-642-31424-7_25"},{"key":"27_CR29","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J.: LTL-constrained steady-state policy synthesis. In: Zhou, Z. (ed.) Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event \/ Montreal, Canada, 19-27 August 2021. pp. 4104\u20134111. ijcai.org (2021). https:\/\/doi.org\/10.24963\/IJCAI.2021\/565","DOI":"10.24963\/IJCAI.2021\/565"},{"key":"27_CR30","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":"27_CR31","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: TACAS. Lecture Notes in Computer Science, vol.\u00a06015, pp. 23\u201337. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_3","DOI":"10.1007\/978-3-642-12002-2_3"},{"key":"27_CR32","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS. pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"27_CR33","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":"27_CR34","unstructured":"Quatmann, T.: Verification of multi-objective Markov models. Ph.D. thesis, RWTH Aachen University, Germany (2023), https:\/\/publications.rwth-aachen.de\/record\/971553"},{"key":"27_CR35","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.: Multi-objective optimization of long-run average and total rewards. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12651, pp. 230\u2013249. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_13","DOI":"10.1007\/978-3-030-72016-2_13"},{"key":"27_CR36","doi-asserted-by":"publisher","unstructured":"Randour, M., Raskin, J., Sankur, O.: Percentile queries in multi-dimensional Markov decision processes. Formal Methods Syst. Des. 50(2-3), 207\u2013248 (2017). https:\/\/doi.org\/10.1007\/S10703-016-0262-7","DOI":"10.1007\/S10703-016-0262-7"},{"key":"27_CR37","doi-asserted-by":"publisher","unstructured":"Sickert, S., Esparza, J., Jaax, S., Kret\u00ednsk\u00fd, J.: Limit-deterministic B\u00fcchi automata for linear temporal logic. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol.\u00a09780, pp. 312\u2013332. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17","DOI":"10.1007\/978-3-319-41540-6_17"},{"key":"27_CR38","doi-asserted-by":"publisher","unstructured":"Svorenov\u00e1, M., Cerna, I., Belta, C.: Optimal control of MDPs with temporal logic constraints. In: Proceedings of the 52nd IEEE Conference on Decision and Control, CDC 2013, Florence, Italy, December 10-13, 2013. pp. 3938\u20133943. IEEE (2013). https:\/\/doi.org\/10.1109\/CDC.2013.6760491","DOI":"10.1109\/CDC.2013.6760491"},{"key":"27_CR39","doi-asserted-by":"publisher","unstructured":"Svore\u0148ov\u00e1, M., Cern\u00e1, I., Belta, C.: Optimal receding horizon control for finite deterministic systems with temporal logic constraints. In: American Control Conference, ACC 2013, Washington, DC, USA, June 17-19, 2013. pp. 4399\u20134404. IEEE (2013). https:\/\/doi.org\/10.1109\/ACC.2013.6580517","DOI":"10.1109\/ACC.2013.6580517"},{"key":"27_CR40","doi-asserted-by":"publisher","unstructured":"Velasquez, A., Alkhouri, I., Beckus, A., Trivedi, A., Atia, G.K.: Controller synthesis for omega-regular and steady-state specifications. In: AAMAS. pp. 1310\u20131318. International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS) (2022). https:\/\/doi.org\/10.5555\/3535850.3535996","DOI":"10.5555\/3535850.3535996"}],"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-032-22752-2_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T02:55:21Z","timestamp":1782874521000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22752-2_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227515","9783032227522"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22752-2_27","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":"16 April 2026","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":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}