{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:59:30Z","timestamp":1779087570580,"version":"3.51.4"},"reference-count":68,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2023,3,8]],"date-time":"2023-03-08T00:00:00Z","timestamp":1678233600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,3,8]],"date-time":"2023-03-08T00:00:00Z","timestamp":1678233600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["RTG 2236"],"award-info":[{"award-number":["RTG 2236"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["383882557"],"award-info":[{"award-number":["383882557"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["427755713"],"award-info":[{"award-number":["427755713"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["RTG 2428"],"award-info":[{"award-number":["RTG 2428"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007210","name":"RWTH Aachen University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100007210","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study turn-based stochastic zero-sum games with lexicographic preferences over objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as controllable and adversarial non-determinism. Lexicographic order allows one to consider multiple objectives with a strict preference order. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. For a mixture of reachability and safety objectives, we show that deterministic lexicographically optimal strategies exist and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{NP}\\cap \\textsf{coNP}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>NP<\/mml:mi>\n                    <mml:mo>\u2229<\/mml:mo>\n                    <mml:mi>coNP<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, matching the current known bound for single objectives; and in general the decision problem is <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{PSPACE}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>PSPACE<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-hard and can be solved in <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{NEXPTIME}\\cap \\textsf{coNEXPTIME}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>NEXPTIME<\/mml:mi>\n                    <mml:mo>\u2229<\/mml:mo>\n                    <mml:mi>coNEXPTIME<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. We present an algorithm that computes the lexicographically optimal strategies via a reduction to the computation of optimal strategies in a sequence of single-objectives games. For omega-regular objectives, we restrict our analysis to one-player games, also known as Markov decision processes. We show that lexicographically optimal strategies exist and need either randomization or finite memory. We present an algorithm that solves the relevant decision problem in polynomial time. We have implemented our algorithms and report experimental results on various case studies.<\/jats:p>","DOI":"10.1007\/s10703-023-00411-4","type":"journal-article","created":{"date-parts":[[2023,3,8]],"date-time":"2023-03-08T12:06:13Z","timestamp":1678277173000},"page":"40-80","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Stochastic games with lexicographic objectives"],"prefix":"10.1007","volume":"63","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4561-241X","authenticated-orcid":false,"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8630-3218","authenticated-orcid":false,"given":"Stefanie","family":"Mohr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0163-2152","authenticated-orcid":false,"given":"Maximilian","family":"Weininger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1084-6408","authenticated-orcid":false,"given":"Tobias","family":"Winkler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,3,8]]},"reference":[{"issue":"2","key":"411_CR1","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A Condon","year":"1992","unstructured":"Condon A (1992) The complexity of stochastic games. Inf Comput 96(2):203\u2013224. https:\/\/doi.org\/10.1016\/0890-5401(92)90048-K","journal-title":"Inf Comput"},{"key":"411_CR2","volume-title":"Markov decision processes: discrete stochastic dynamic programming","author":"ML Puterman","year":"2014","unstructured":"Puterman ML (2014) Markov decision processes: discrete stochastic dynamic programming. Wiley, New Jersey"},{"key":"411_CR3","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Massachusetts"},{"key":"411_CR4","volume-title":"Competitive markov decision processes","author":"J Filar","year":"1997","unstructured":"Filar J, Vrieze K (1997) Competitive markov decision processes. Springer, Switzerland"},{"issue":"2","key":"411_CR5","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1016\/j.jcss.2011.05.002","volume":"78","author":"K Chatterjee","year":"2012","unstructured":"Chatterjee K, Henzinger TA (2012) A survey of stochastic $$\\omega $$-regular games. J Comput Syst Sci 78(2):394\u2013413. https:\/\/doi.org\/10.1016\/j.jcss.2011.05.002","journal-title":"J Comput Syst Sci"},{"key":"411_CR6","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Sen K, Henzinger TA (2008) Model-checking omega-regular properties of interval Markov chains. In: FoSSaCS. Lecture notes in computer science, vol 4962, Springer, Switzerland, pp 302\u2013317","DOI":"10.1007\/978-3-540-78499-9_22"},{"key":"411_CR7","doi-asserted-by":"publisher","unstructured":"Weininger M, Meggendorfer T, Kret\u00ednsk\u00fd J (2019) Satisfiability bounds for $$\\omega $$-regular properties in bounded-parameter Markov decision processes. In: CDC, IEEE, New York, pp, 2284\u20132291, doi: https:\/\/doi.org\/10.1109\/CDC40024.2019.9029460","DOI":"10.1109\/CDC40024.2019.9029460"},{"key":"411_CR8","volume-title":"Constrained Markov decision processes","author":"E Altman","year":"1999","unstructured":"Altman E (1999) Constrained Markov decision processes. CRC Press, Florida"},{"key":"411_CR9","doi-asserted-by":"publisher","unstructured":"Chatterjee K (2007) Markov decision processes with multiple long-run average objectives. In: FSTTCS. Lecture notes in computer science, vol 4855, Springer, Switzerland, pp 473\u2013484, doi: https:\/\/doi.org\/10.1007\/978-3-540-77050-3_39","DOI":"10.1007\/978-3-540-77050-3_39"},{"key":"411_CR10","doi-asserted-by":"publisher","unstructured":"Delgrange F, Katoen J, Quatmann T, Randour M (2020) Simple strategies in multi-objective MDPs. In: TACAS (1). Lecture notes in computer science, vol 12078, Springer, Switzerland, pp 346\u2013364, doi: https:\/\/doi.org\/10.1007\/978-3-030-45190-5_19","DOI":"10.1007\/978-3-030-45190-5_19"},{"key":"411_CR11","doi-asserted-by":"publisher","unstructured":"Berthon R, Guha S, Raskin J (2020) Mixing probabilistic and non-probabilistic objectives in markov decision processes. In: LICS, ACM, New York, pp 195\u2013208, doi: https:\/\/doi.org\/10.1145\/3373718.3394805","DOI":"10.1145\/3373718.3394805"},{"key":"411_CR12","doi-asserted-by":"publisher","unstructured":"Chen T, Forejt V, Kwiatkowska MZ, Simaitis A, Wiltsche C (2013) On stochastic games with multiple objectives. In: MFCS. Lecture notes in computer science, vol 8087, Springer, Switzerland, pp 266\u2013277, doi: https:\/\/doi.org\/10.1007\/978-3-642-40313-2_25","DOI":"10.1007\/978-3-642-40313-2_25"},{"issue":"11","key":"411_CR13","doi-asserted-by":"publisher","first-page":"1442","DOI":"10.1287\/mnsc.20.11.1442","volume":"20","author":"PC Fishburn","year":"1974","unstructured":"Fishburn PC (1974) Exceptional paper - lexicographic orders, utilities and decision rules: a survey. Manage Sci 20(11):1442\u20131471. https:\/\/doi.org\/10.1287\/mnsc.20.11.1442","journal-title":"Manage Sci"},{"key":"411_CR14","doi-asserted-by":"publisher","DOI":"10.2307\/2938240","author":"L Blume","year":"1991","unstructured":"Blume L, Brandenburger A, Dekel E (1991) Lexicographic probabilities and choice under uncertainty. Econom: J Econom Soc. https:\/\/doi.org\/10.2307\/2938240","journal-title":"Econom: J Econom Soc"},{"key":"411_CR15","doi-asserted-by":"publisher","unstructured":"Bloem R, Chatterjee K, Henzinger TA, Jobstmann B (2009) Better quality in synthesis through quantitative objectives. In: CAV. Lecture notes in computer science, vol 5643, Springer, Switzerland, pp 140\u2013156, doi: https:\/\/doi.org\/10.1007\/978-3-642-02658-4_14","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"411_CR16","doi-asserted-by":"publisher","unstructured":"Colcombet T, Jurdzinski M, Lazic R, Schmitz S (2017) Perfect half space games. In: Logic in Computer Science, LICS 2017, IEEE Computer Society, Washington, DC, pp 1\u201311, doi: https:\/\/doi.org\/10.1109\/LICS.2017.8005105","DOI":"10.1109\/LICS.2017.8005105"},{"key":"411_CR17","doi-asserted-by":"publisher","unstructured":"Wray KH, Zilberstein S, Mouaddib A (2015) Multi-objective MDPs with conditional lexicographic reward preferences. In: AAAI, AAAI Press, California, pp 3418\u20133424, doi: https:\/\/doi.org\/10.5555\/2888116.2888191","DOI":"10.5555\/2888116.2888191"},{"key":"411_CR18","doi-asserted-by":"publisher","unstructured":"Hahn EM, Perez M, Schewe S, Somenzi F, Trivedi A, Wojtczak D (2021) Model-free reinforcement learning for lexicographic omega-regular objectives. In: FM. Lecture Notes in Computer Science, vol 13047, Springer, Switzerland , pp 142\u2013159, doi: https:\/\/doi.org\/10.1007\/978-3-030-90870-6_8","DOI":"10.1007\/978-3-030-90870-6_8"},{"key":"411_CR19","doi-asserted-by":"publisher","unstructured":"Chatterjee K, Katoen J, Weininger M, Winkler T (2020) Stochastic games with lexicographic reachability-safety objectives. In: CAV (2). Lecture notes in computer science, vol 12225, Springer, Switzerland, pp 398\u2013420, doi: https:\/\/doi.org\/10.1007\/978-3-030-53291-8_21","DOI":"10.1007\/978-3-030-53291-8_21"},{"key":"411_CR20","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(1:11)2022","author":"P Bouyer","year":"2022","unstructured":"Bouyer P, Roux SL, Oualhadj Y, Randour M, Vandenhove P (2022) Games where you can play optimally with arena-independent finite memory. Log Methods Comput Sci. https:\/\/doi.org\/10.46298\/lmcs-18(1:11)2022","journal-title":"Log Methods Comput Sci"},{"key":"411_CR21","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:8)2008","author":"K Etessami","year":"2008","unstructured":"Etessami K, Kwiatkowska MZ, Vardi MY, Yannakakis M (2008) Multi-objective model checking of Markov decision processes. LMCS. https:\/\/doi.org\/10.2168\/LMCS-4(4:8)2008","journal-title":"LMCS"},{"key":"411_CR22","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(1:13)2014","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil T, Brozek V, Chatterjee K, Forejt V, Kucera A (2014) Two views on multiple mean-payoff objectives in Markov decision processes. LMCS. https:\/\/doi.org\/10.2168\/LMCS-10(1:13)2014","journal-title":"LMCS"},{"key":"411_CR23","doi-asserted-by":"publisher","unstructured":"Chatterjee K, Forejt V, Wojtczak D (2013) Multi-objective discounted reward verification in graphs and mdps. In: LPAR. Lecture notes in computer science, vol 8312, Springer, Switzerland, pp 228\u2013242, https:\/\/doi.org\/10.1007\/978-3-642-45221-5_17","DOI":"10.1007\/978-3-642-45221-5_17"},{"key":"411_CR24","doi-asserted-by":"publisher","unstructured":"Forejt V, Kwiatkowska MZ, Norman G, Parker D, Qu H (2011) Quantitative multi-objective verification for probabilistic systems. In: TACAS, pp 112\u2013127 . doi: https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11","DOI":"10.1007\/978-3-642-19835-9_11"},{"key":"411_CR25","doi-asserted-by":"publisher","unstructured":"Quatmann T, Katoen J (2021) Multi-objective optimization of long-run average and total rewards. In: TACAS (1). Lecture notes in computer science, vol 12651, Springer, Switzerland, pp 230\u2013249, doi: https:\/\/doi.org\/10.1007\/978-3-030-72016-2_13","DOI":"10.1007\/978-3-030-72016-2_13"},{"key":"411_CR26","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/j.jcss.2016.09.009","volume":"84","author":"T Br\u00e1zdil","year":"2017","unstructured":"Br\u00e1zdil T, Chatterjee K, Forejt V, Kucera A (2017) Trading performance for stability in markov decision processes. J Comput Syst Sci 84:144\u2013170. https:\/\/doi.org\/10.1016\/j.jcss.2016.09.009","journal-title":"J Comput Syst Sci"},{"issue":"1","key":"411_CR27","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1109\/9.362904","volume":"40","author":"JA Filar","year":"1995","unstructured":"Filar JA, Krass D, Ross KW (1995) Percentile performance criteria for limiting average Markov decision processes. IEEE Trans Autom Control 40(1):2\u201310","journal-title":"IEEE Trans Autom Control"},{"issue":"2\u20133","key":"411_CR28","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/s10703-016-0262-7","volume":"50","author":"M Randour","year":"2017","unstructured":"Randour M, Raskin J, Sankur O (2017) Percentile queries in multi-dimensional Markov decision processes. Formal Methods Syst Des 50(2\u20133):207\u2013248. https:\/\/doi.org\/10.1007\/s10703-016-0262-7","journal-title":"Formal Methods Syst Des"},{"key":"411_CR29","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(2:15)2017","author":"K Chatterjee","year":"2017","unstructured":"Chatterjee K, Kret\u00ednsk\u00e1 Z, Kret\u00ednsk\u00fd J (2017) Unifying two views on multiple mean-payoff objectives in Markov decision processes. LMCS. https:\/\/doi.org\/10.23638\/LMCS-13(2:15)2017","journal-title":"LMCS"},{"key":"411_CR30","doi-asserted-by":"publisher","unstructured":"Baier C, Dubslaff C, Kl\u00fcppelholz S (2014) Trade-off analysis meets probabilistic model checking. In: CSL-LICS, pp 1\u20131110, doi: https:\/\/doi.org\/10.1145\/2603088.2603089","DOI":"10.1145\/2603088.2603089"},{"key":"411_CR31","doi-asserted-by":"publisher","unstructured":"Baier C, Dubslaff C, Kl\u00fcppelholz S, Daum M, Klein J, M\u00e4rcker S, Wunderlich S (2014) Probabilistic model checking and non-standard multi-objective reasoning. In: FASE. Lecture notes in computer science, vol 8411, Springer, Switzerland, pp 1\u201316, doi: https:\/\/doi.org\/10.1007\/978-3-642-54804-8_1","DOI":"10.1007\/978-3-642-54804-8_1"},{"key":"411_CR32","doi-asserted-by":"publisher","DOI":"10.2200\/S00765ED1V01Y201704AIM034","author":"DM Roijers","year":"2017","unstructured":"Roijers DM, Whiteson S (2017) Multi-objective decision making. Synth Lect Artif Intell Mach Learn. https:\/\/doi.org\/10.2200\/S00765ED1V01Y201704AIM034","journal-title":"Synth Lect Artif Intell Mach Learn"},{"key":"411_CR33","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.ejcon.2016.04.009","volume":"30","author":"M Svorenov\u00e1","year":"2016","unstructured":"Svorenov\u00e1 M, Kwiatkowska M (2016) Quantitative verification and strategy synthesis for stochastic games. Eur J Control 30:15\u201330. https:\/\/doi.org\/10.1016\/j.ejcon.2016.04.009","journal-title":"Eur J Control"},{"key":"411_CR34","doi-asserted-by":"publisher","unstructured":"Basset N, Kwiatkowska MZ, Topcu U, Wiltsche C (2015) Strategy synthesis for stochastic games with multiple long-run objectives. In: TACAS. Lecture notes in computer science, vol 9035, Springer, Switzerland, pp 256\u2013271, doi: https:\/\/doi.org\/10.1007\/978-3-662-46681-0_22","DOI":"10.1007\/978-3-662-46681-0_22"},{"key":"411_CR35","doi-asserted-by":"publisher","unstructured":"Chatterjee K, Doyen L (2016) Perfect-information stochastic games with generalized mean-payoff objectives. In: LICS, ACM, New York, pp 247\u2013256, doi: https:\/\/doi.org\/10.1145\/2933575.2934513","DOI":"10.1145\/2933575.2934513"},{"key":"411_CR36","doi-asserted-by":"publisher","unstructured":"Brenguier R, Forejt V (2016) Decidability results for multi-objective stochastic games. In: ATVA. Lecture notes in computer science, vol 9938, pp 227\u2013243, doi: https:\/\/doi.org\/10.1007\/978-3-319-46520-3_15","DOI":"10.1007\/978-3-319-46520-3_15"},{"key":"411_CR37","doi-asserted-by":"publisher","unstructured":"Chen T, Kwiatkowska MZ, Simaitis A, Wiltsche C (2013) Synthesis for multi-objective stochastic games: An application to autonomous urban driving. In: QEST, pp 322\u2013337, doi: https:\/\/doi.org\/10.1007\/978-3-642-40196-1_28","DOI":"10.1007\/978-3-642-40196-1_28"},{"key":"411_CR38","doi-asserted-by":"publisher","unstructured":"Ashok P, Chatterjee K, Kret\u00ednsk\u00fd J, Weininger M, Winkler T (2020) Approximating values of generalized-reachability stochastic games. In: LICS, ACM, New York, pp 102\u2013115, doi: https:\/\/doi.org\/10.1145\/3373718.3394761","DOI":"10.1145\/3373718.3394761"},{"key":"411_CR39","doi-asserted-by":"publisher","unstructured":"Bruy\u00e8re V, Hautem Q, Raskin J (2018) Parameterized complexity of games with monotonically ordered omega-regular objectives. In: CONCUR. LIPIcs, vol 118, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Wadern . pp 29\u201312916, doi: https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.29","DOI":"10.4230\/LIPIcs.CONCUR.2018.29"},{"key":"411_CR40","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/j.ic.2016.10.011","volume":"254","author":"V Bruy\u00e8re","year":"2017","unstructured":"Bruy\u00e8re V, Filiot E, Randour M, Raskin J (2017) Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games. Inf Comput 254:259\u2013295. https:\/\/doi.org\/10.1016\/j.ic.2016.10.011","journal-title":"Inf Comput"},{"key":"411_CR41","unstructured":"Wray KH, Zilberstein S (2015) Multi-objective POMDPs with lexicographic reward preferences. In: IJCAI, AAAI Press, California, pp 1719\u20131725, http:\/\/ijcai.org\/Abstract\/15\/245"},{"issue":"2","key":"411_CR42","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10009-017-0476-z","volume":"20","author":"M Kwiatkowska","year":"2018","unstructured":"Kwiatkowska M, Parker D, Wiltsche C (2018) PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. STTT 20(2):195\u2013210. https:\/\/doi.org\/10.1007\/s10009-017-0476-z","journal-title":"STTT"},{"key":"411_CR43","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil T, Chatterjee K, Forejt V, Kucera A (2015) MultiGain: a controller synthesis tool for MDPs with multiple mean-payoff objectives. In: TACAS. lecture notes in computer science, vol 9035, Springer, Switzerland, pp 181\u2013187, doi: https:\/\/doi.org\/10.1007\/978-3-662-46681-0_12","DOI":"10.1007\/978-3-662-46681-0_12"},{"key":"411_CR44","doi-asserted-by":"publisher","unstructured":"Dehnert C, Junges S, Katoen J, Volk M (2017) A storm is coming: A modern probabilistic model checker. In: CAV (2). Lecture notes in computer science, vol 10427, Springer, Switzerland pp. 592\u2013600, doi: https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"411_CR45","doi-asserted-by":"publisher","unstructured":"Quatmann T, Junges S, Katoen J (2017) Markov automata with multiple objectives. In: CAV (1). Lecture Notes in Computer Science, vol 10426, Springer, Switzerland, pp 140\u2013159, doi: https:\/\/doi.org\/10.1007\/978-3-319-63387-9_7","DOI":"10.1007\/978-3-319-63387-9_7"},{"key":"411_CR46","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 (2020) Multi-cost bounded tradeoff analysis in MDP 64:1483\u20131522. https:\/\/doi.org\/10.1007\/s10817-020-09574-9","journal-title":"Multi-cost bounded tradeoff analysis in MDP"},{"key":"411_CR47","doi-asserted-by":"publisher","unstructured":"Pranger S, K\u00f6nighofer B, Posch L, Bloem R (2021) TEMPEST - synthesis tool for reactive systems and shields in probabilistic environments. In: ATVA. Lecture notes in computer science, vol 12971, Springer, Switzerland, pp 222\u2013228, doi: https:\/\/doi.org\/10.1007\/978-3-030-88885-5_15","DOI":"10.1007\/978-3-030-88885-5_15"},{"issue":"2","key":"411_CR48","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pacific J Math 5(2):285\u2013309. https:\/\/doi.org\/10.2140\/pjm.1955.5.285","journal-title":"Pacific J Math"},{"key":"411_CR49","doi-asserted-by":"publisher","unstructured":"Forejt V, Kwiatkowska MZ, Parker D (2012) Pareto curves for probabilistic model checking. In: ATVA. Lecture notes in computer science, vol 7561, Springer, Switzerland, pp. 317\u2013332, doi: https:\/\/doi.org\/10.1007\/978-3-642-33386-6_25","DOI":"10.1007\/978-3-642-33386-6_25"},{"key":"411_CR50","unstructured":"Fijalkow N, Horn F (2010) The surprizing complexity of reachability games. CoRR abs\/1010.2420arxiv:1010.2420"},{"key":"411_CR51","doi-asserted-by":"publisher","unstructured":"Winkler T, Weininger M (2021) Stochastic games with disjunctions of multiple objectives. In: GandALF. EPTCS, vol 346, pp 83\u2013100, doi: https:\/\/doi.org\/10.4204\/EPTCS.346.6","DOI":"10.4204\/EPTCS.346.6"},{"key":"411_CR52","doi-asserted-by":"publisher","unstructured":"Kupferman O, Vardi MY (1998)Freedom, weakness, and determinism: From linear-time to branching-time. In: LICS, IEEE Computer Society, Washington, DC, pp 81\u201392, doi: https:\/\/doi.org\/10.1109\/LICS.1998.705645","DOI":"10.1109\/LICS.1998.705645"},{"key":"411_CR53","unstructured":"Sickert S (2019) A unified translation of linear temporal logic to $$\\omega $$-automata. PhD thesis, Technical University of Munich, Germany https:\/\/nbn-resolving.org\/urn:nbn:de:bvb:91-diss-20190801-1484932-1-4"},{"key":"411_CR54","doi-asserted-by":"publisher","unstructured":"Chatterjee K, Henzinger M (2011) Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: SODA, SIAM, Philadelphia, pp 1318\u20131336, doi: https:\/\/doi.org\/10.1137\/1.9781611973082.101","DOI":"10.1137\/1.9781611973082.101"},{"key":"411_CR55","doi-asserted-by":"publisher","unstructured":"Chatterjee K, Dvor\u00e1k W, Henzinger M, Loitzenbauer V (2016) Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. In: LICS, ACM, New York, pp197\u2013206, doi: https:\/\/doi.org\/10.1145\/2933575.2935304","DOI":"10.1145\/2933575.2935304"},{"key":"411_CR56","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Dvor\u00e1k W, Henzinger M, Loitzenbauer V (2016) Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. CoRR abs\/1602.02670arxiv:1602.02670","DOI":"10.1145\/2933575.2935304"},{"key":"411_CR57","doi-asserted-by":"publisher","unstructured":"Kelmendi E, Kr\u00e4mer J, Kret\u00ednsk\u00fd J, Weininger M (2018) Value iteration for simple stochastic games: stopping criterion and learning algorithm. In: CAV (1). Lecture notes in computer science, vol 10981, Springer, Switzerland, pp. 623\u2013642, doi: https:\/\/doi.org\/10.1007\/978-3-319-96145-3_36","DOI":"10.1007\/978-3-319-96145-3_36"},{"key":"411_CR58","doi-asserted-by":"publisher","unstructured":"van Dijk T (2018) Attracting tangles to solve parity games. In: CAV (2). Lecture notes in computer science, vol 10982, Springer, Switzerland, pp 198\u2013215, doi: https:\/\/doi.org\/10.1007\/978-3-319-96142-2_14","DOI":"10.1007\/978-3-319-96142-2_14"},{"key":"411_CR59","unstructured":"Ujma M (2015) On verification and controller synthesis for probabilistic systems at runtime. PhD thesis, University of Oxford, UK http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.711811"},{"key":"411_CR60","doi-asserted-by":"publisher","unstructured":"L\u00f6ding C (1999) Optimal bounds for transformations of omega-automata. In: FSTTCS. Lecture notes in computer science, vol 1738, Springer, Switzerland, pp 97\u2013109, doi: https:\/\/doi.org\/10.1007\/3-540-46691-6_8","DOI":"10.1007\/3-540-46691-6_8"},{"key":"411_CR61","doi-asserted-by":"publisher","unstructured":"M\u00fcller D, Sickert S (2017) LTL to deterministic emerson-lei automata. In: GandALF. EPTCS, vol 256, pp 180\u2013194, doi: https:\/\/doi.org\/10.4204\/EPTCS.256.13","DOI":"10.4204\/EPTCS.256.13"},{"key":"411_CR62","doi-asserted-by":"publisher","unstructured":"Littman ML, Cassandra AR, Kaelbling LP (1995) Learning policies for partially observable environments: Scaling up. In: ICML, Morgan Kaufmann, Massachusetts, pp 362\u2013370, doi: https:\/\/doi.org\/10.1016\/b978-1-55860-377-6.50052-9","DOI":"10.1016\/b978-1-55860-377-6.50052-9"},{"key":"411_CR63","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.artint.2016.01.007","volume":"234","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee K, Chmelik M, Gupta R, Kanodia A (2016) Optimal cost almost-sure reachability in POMDPs. Artif Intell 234:26\u201348. https:\/\/doi.org\/10.1016\/j.artint.2016.01.007","journal-title":"Artif Intell"},{"key":"411_CR64","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1016\/j.artint.2014.12.009","volume":"221","author":"K Chatterjee","year":"2015","unstructured":"Chatterjee K, Chmel\u00edk M (2015) POMDPs under probabilistic semantics. Artif Intell 221:46\u201372. https:\/\/doi.org\/10.1016\/j.artint.2014.12.009","journal-title":"Artif Intell"},{"key":"411_CR65","doi-asserted-by":"publisher","unstructured":"Duret-Lutz A, Lewkowicz A, Fauchille A, Michaud T, Renault E, Xu L (2016) Spot 2.0 - A framework for LTL and $$\\omega $$-automata manipulation. In: ATVA. Lecture notes in computer science, vol 9938, pp 122\u2013129, doi: https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8","DOI":"10.1007\/978-3-319-46520-3_8"},{"issue":"12","key":"411_CR66","doi-asserted-by":"publisher","first-page":"1272","DOI":"10.1016\/j.tcs.2008.12.058","volume":"410","author":"M Kwiatkowska","year":"2009","unstructured":"Kwiatkowska M, Norman G, Parker D, Vigliotti MG (2009) Probabilistic mobile ambients. Theor Comput Sci 410(12):1272\u20131303. https:\/\/doi.org\/10.1016\/j.tcs.2008.12.058","journal-title":"Theor Comput Sci"},{"key":"411_CR67","doi-asserted-by":"publisher","unstructured":"Feng L, Wiltsche C, Humphrey LR, Topcu U (2015) Controller synthesis for autonomous systems interacting with human operators. In: ICCPS, ACM, New York, pp 70\u201379, doi: https:\/\/doi.org\/10.1145\/2735960.2735973","DOI":"10.1145\/2735960.2735973"},{"key":"411_CR68","unstructured":"Chatterjee K, Piterman N (2019) Combinations of qualitative winning for stochastic parity games. In: CONCUR. LIPIcs, vol 140, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Wadern, pp 6\u20131617, doi: 0.4230\/LIPIcs.CONCUR.2019.6"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00411-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00411-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00411-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,21]],"date-time":"2024-10-21T17:11:59Z","timestamp":1729530719000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00411-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,8]]},"references-count":68,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["411"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00411-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,3,8]]},"assertion":[{"value":"3 January 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 January 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 March 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}