[{"license":"https://creativecommons.org/licenses/by/4.0/","day":"08","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Joost P","last_name":"Katoen","id":"4524F760-F248-11E8-B48F-1D18A9856A87","full_name":"Katoen, Joost P"},{"first_name":"Stefanie","last_name":"Mohr","full_name":"Mohr, Stefanie"},{"last_name":"Weininger","first_name":"Maximilian","full_name":"Weininger, Maximilian"},{"last_name":"Winkler","first_name":"Tobias","full_name":"Winkler, Tobias"}],"title":"Stochastic games with lexicographic objectives","department":[{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer Nature","article_processing_charge":"No","ec_funded":1,"scopus_import":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"article_type":"original","publication":"Formal Methods in System Design","publication_identifier":{"eissn":["1572-8102"]},"quality_controlled":"1","doi":"10.1007/s10703-023-00411-4","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}],"isi":1,"abstract":[{"text":"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 NP∩coNP, matching the current known bound for single objectives; and in general the decision problem is PSPACE-hard and can be solved in NEXPTIME∩coNEXPTIME. 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.","lang":"eng"}],"date_updated":"2025-07-14T09:10:14Z","month":"03","type":"journal_article","oa_version":"Published Version","date_created":"2023-03-19T23:00:59Z","year":"2023","acknowledgement":"Tobias Winkler and Joost-Pieter Katoen are supported by the DFG RTG 2236 UnRAVeL and the innovation programme under the Marie Skłodowska-Curie grant agreement No. 101008233 (Mission). Krishnendu Chatterjee is supported by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science and Technology Fund (WWTF) Project ICT15-003. Maximilian Weininger is supported by the DFG projects 383882557 Statistical Unbounded Verification (SUV) and 427755713 Group-By Objectives in Probabilistic Verification (GOPro). Stefanie Mohr is supported by the DFG RTG 2428 CONVEY. Open Access funding enabled and organized by Projekt DEAL.","_id":"12738","publication_status":"epub_ahead","oa":1,"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/s10703-023-00411-4"}],"ddc":["000"],"date_published":"2023-03-08T00:00:00Z","status":"public","external_id":{"isi":["000946174300001"]},"citation":{"ama":"Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. Stochastic games with lexicographic objectives. <i>Formal Methods in System Design</i>. 2023. doi:<a href=\"https://doi.org/10.1007/s10703-023-00411-4\">10.1007/s10703-023-00411-4</a>","apa":"Chatterjee, K., Katoen, J. P., Mohr, S., Weininger, M., &#38; Winkler, T. (2023). Stochastic games with lexicographic objectives. <i>Formal Methods in System Design</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10703-023-00411-4\">https://doi.org/10.1007/s10703-023-00411-4</a>","mla":"Chatterjee, Krishnendu, et al. “Stochastic Games with Lexicographic Objectives.” <i>Formal Methods in System Design</i>, Springer Nature, 2023, doi:<a href=\"https://doi.org/10.1007/s10703-023-00411-4\">10.1007/s10703-023-00411-4</a>.","ista":"Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. 2023. Stochastic games with lexicographic objectives. Formal Methods in System Design.","chicago":"Chatterjee, Krishnendu, Joost P Katoen, Stefanie Mohr, Maximilian Weininger, and Tobias Winkler. “Stochastic Games with Lexicographic Objectives.” <i>Formal Methods in System Design</i>. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/s10703-023-00411-4\">https://doi.org/10.1007/s10703-023-00411-4</a>.","ieee":"K. Chatterjee, J. P. Katoen, S. Mohr, M. Weininger, and T. Winkler, “Stochastic games with lexicographic objectives,” <i>Formal Methods in System Design</i>. Springer Nature, 2023.","short":"K. Chatterjee, J.P. Katoen, S. Mohr, M. Weininger, T. Winkler, Formal Methods in System Design (2023)."},"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"8272"}]}},{"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"first_name":"Joost P","last_name":"Katoen","full_name":"Katoen, Joost P","id":"4524F760-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Weininger, Maximilian","first_name":"Maximilian","last_name":"Weininger"},{"full_name":"Winkler, Tobias","last_name":"Winkler","first_name":"Tobias"}],"file":[{"access_level":"open_access","date_created":"2020-08-17T11:32:44Z","checksum":"093d4788d7d5b2ce0ffe64fbe7820043","date_updated":"2020-08-17T11:32:44Z","file_id":"8276","creator":"dernst","relation":"main_file","content_type":"application/pdf","file_size":625056,"success":1,"file_name":"2020_LNCS_CAV_Chatterjee.pdf"}],"day":"14","title":"Stochastic games with lexicographic reachability-safety objectives","arxiv":1,"publisher":"Springer Nature","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","department":[{"_id":"KrCh"}],"publication":"International Conference on Computer Aided Verification","article_processing_charge":"No","ec_funded":1,"scopus_import":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"publication_identifier":{"issn":["03029743"],"eissn":["16113349"],"isbn":["9783030532901"]},"doi":"10.1007/978-3-030-53291-8_21","quality_controlled":"1","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"isi":1,"conference":{"name":"CAV: Computer Aided Verification"},"language":[{"iso":"eng"}],"page":"398-420","abstract":[{"lang":"eng","text":"We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as angelic and demonic non-determinism. Lexicographic order allows to consider multiple objectives with a strict preference order over the satisfaction of the objectives. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. We establish determinacy of such games and present strategy and computational complexity results. For strategy complexity, we show that lexicographically optimal strategies exist that are deterministic 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   NP∩coNP , matching the current known bound for single objectives; and in general the decision problem is   PSPACE -hard and can be solved in   NEXPTIME∩coNEXPTIME . We present an algorithm that computes the lexicographically optimal strategies via a reduction to computation of optimal strategies in a sequence of single-objectives games. We have implemented our algorithm and report experimental results on various case studies."}],"date_updated":"2025-07-14T09:10:14Z","month":"07","oa_version":"Published Version","type":"conference","volume":12225,"file_date_updated":"2020-08-17T11:32:44Z","date_created":"2020-08-16T22:00:58Z","year":"2020","_id":"8272","publication_status":"published","oa":1,"has_accepted_license":"1","ddc":["000"],"date_published":"2020-07-14T00:00:00Z","alternative_title":["LNCS"],"external_id":{"isi":["000695272500021"],"arxiv":["2005.04018"]},"status":"public","related_material":{"record":[{"relation":"later_version","id":"12738","status":"public"}]},"intvolume":"     12225","citation":{"mla":"Chatterjee, Krishnendu, et al. “Stochastic Games with Lexicographic Reachability-Safety Objectives.” <i>International Conference on Computer Aided Verification</i>, vol. 12225, Springer Nature, 2020, pp. 398–420, doi:<a href=\"https://doi.org/10.1007/978-3-030-53291-8_21\">10.1007/978-3-030-53291-8_21</a>.","ista":"Chatterjee K, Katoen JP, Weininger M, Winkler T. 2020. Stochastic games with lexicographic reachability-safety objectives. International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 12225, 398–420.","apa":"Chatterjee, K., Katoen, J. P., Weininger, M., &#38; Winkler, T. (2020). Stochastic games with lexicographic reachability-safety objectives. In <i>International Conference on Computer Aided Verification</i> (Vol. 12225, pp. 398–420). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-53291-8_21\">https://doi.org/10.1007/978-3-030-53291-8_21</a>","ama":"Chatterjee K, Katoen JP, Weininger M, Winkler T. Stochastic games with lexicographic reachability-safety objectives. In: <i>International Conference on Computer Aided Verification</i>. Vol 12225. Springer Nature; 2020:398-420. doi:<a href=\"https://doi.org/10.1007/978-3-030-53291-8_21\">10.1007/978-3-030-53291-8_21</a>","short":"K. Chatterjee, J.P. Katoen, M. Weininger, T. Winkler, in:, International Conference on Computer Aided Verification, Springer Nature, 2020, pp. 398–420.","ieee":"K. Chatterjee, J. P. Katoen, M. Weininger, and T. Winkler, “Stochastic games with lexicographic reachability-safety objectives,” in <i>International Conference on Computer Aided Verification</i>, 2020, vol. 12225, pp. 398–420.","chicago":"Chatterjee, Krishnendu, Joost P Katoen, Maximilian Weininger, and Tobias Winkler. “Stochastic Games with Lexicographic Reachability-Safety Objectives.” In <i>International Conference on Computer Aided Verification</i>, 12225:398–420. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/978-3-030-53291-8_21\">https://doi.org/10.1007/978-3-030-53291-8_21</a>."}},{"title":"Parameter-independent strategies for pMDPs via POMDPs","arxiv":1,"publist_id":"7975","author":[{"last_name":"Arming","first_name":"Sebastian","full_name":"Arming, Sebastian"},{"full_name":"Bartocci, Ezio","last_name":"Bartocci","first_name":"Ezio"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Joost P","last_name":"Katoen","id":"4524F760-F248-11E8-B48F-1D18A9856A87","full_name":"Katoen, Joost P"},{"full_name":"Sokolova, Ana","first_name":"Ana","last_name":"Sokolova"}],"day":"15","article_processing_charge":"No","scopus_import":"1","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"doi":"10.1007/978-3-319-99154-2_4","quality_controlled":"1","conference":{"end_date":"2018-09-07","name":"QEST: Quantitative Evaluation of Systems","location":"Beijing, China","start_date":"2018-09-04"},"isi":1,"language":[{"iso":"eng"}],"volume":11024,"date_created":"2018-12-11T11:44:31Z","page":"53-70","oa_version":"Preprint","type":"conference","month":"08","date_updated":"2023-09-13T09:38:28Z","abstract":[{"text":"Markov Decision Processes (MDPs) are a popular class of models suitable for solving control decision problems in probabilistic reactive systems. We consider parametric MDPs (pMDPs) that include parameters in some of the transition probabilities to account for stochastic uncertainties of the environment such as noise or input disturbances. We study pMDPs with reachability objectives where the parameter values are unknown and impossible to measure directly during execution, but there is a probability distribution known over the parameter values. We study for the first time computing parameter-independent strategies that are expectation optimal, i.e., optimize the expected reachability probability under the probability distribution over the parameters. We present an encoding of our problem to partially observable MDPs (POMDPs), i.e., a reduction of our problem to computing optimal strategies in POMDPs. We evaluate our method experimentally on several benchmarks: a motivating (repeated) learner model; a series of benchmarks of varying configurations of a robot moving on a grid; and a consensus protocol.","lang":"eng"}],"_id":"79","year":"2018","date_published":"2018-08-15T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1806.05126","open_access":"1"}],"oa":1,"publication_status":"published","intvolume":"     11024","citation":{"ama":"Arming S, Bartocci E, Chatterjee K, Katoen JP, Sokolova A. Parameter-independent strategies for pMDPs via POMDPs. In: Vol 11024. Springer; 2018:53-70. doi:<a href=\"https://doi.org/10.1007/978-3-319-99154-2_4\">10.1007/978-3-319-99154-2_4</a>","ista":"Arming S, Bartocci E, Chatterjee K, Katoen JP, Sokolova A. 2018. Parameter-independent strategies for pMDPs via POMDPs. QEST: Quantitative Evaluation of Systems, LNCS, vol. 11024, 53–70.","mla":"Arming, Sebastian, et al. <i>Parameter-Independent Strategies for PMDPs via POMDPs</i>. Vol. 11024, Springer, 2018, pp. 53–70, doi:<a href=\"https://doi.org/10.1007/978-3-319-99154-2_4\">10.1007/978-3-319-99154-2_4</a>.","apa":"Arming, S., Bartocci, E., Chatterjee, K., Katoen, J. P., &#38; Sokolova, A. (2018). Parameter-independent strategies for pMDPs via POMDPs (Vol. 11024, pp. 53–70). Presented at the QEST: Quantitative Evaluation of Systems, Beijing, China: Springer. <a href=\"https://doi.org/10.1007/978-3-319-99154-2_4\">https://doi.org/10.1007/978-3-319-99154-2_4</a>","ieee":"S. Arming, E. Bartocci, K. Chatterjee, J. P. Katoen, and A. Sokolova, “Parameter-independent strategies for pMDPs via POMDPs,” presented at the QEST: Quantitative Evaluation of Systems, Beijing, China, 2018, vol. 11024, pp. 53–70.","chicago":"Arming, Sebastian, Ezio Bartocci, Krishnendu Chatterjee, Joost P Katoen, and Ana Sokolova. “Parameter-Independent Strategies for PMDPs via POMDPs,” 11024:53–70. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-99154-2_4\">https://doi.org/10.1007/978-3-319-99154-2_4</a>.","short":"S. Arming, E. Bartocci, K. Chatterjee, J.P. Katoen, A. Sokolova, in:, Springer, 2018, pp. 53–70."},"alternative_title":["LNCS"],"status":"public","external_id":{"isi":["000548912200004"],"arxiv":["1806.05126"]}},{"date_published":"2017-12-07T00:00:00Z","main_file_link":[{"open_access":"1","url":"https://dl.acm.org/doi/10.1145/3158121"}],"publication_status":"published","oa":1,"intvolume":"         2","citation":{"ista":"Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.","mla":"Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL, 33, Association for Computing Machinery, 2017, doi:<a href=\"https://doi.org/10.1145/3158121\">10.1145/3158121</a>.","apa":"Mciver, A., Morgan, C., Kaminski, B. L., &#38; Katoen, J. P. (2017). A new proof rule for almost-sure termination. <i>Proceedings of the ACM on Programming Languages</i>. Los Angeles, CA, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3158121\">https://doi.org/10.1145/3158121</a>","ama":"Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure termination. <i>Proceedings of the ACM on Programming Languages</i>. 2017;2(POPL). doi:<a href=\"https://doi.org/10.1145/3158121\">10.1145/3158121</a>","short":"A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017).","ieee":"A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule for almost-sure termination,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL. Association for Computing Machinery, 2017.","chicago":"Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost P Katoen. “A New Proof Rule for Almost-Sure Termination.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2017. <a href=\"https://doi.org/10.1145/3158121\">https://doi.org/10.1145/3158121</a>."},"external_id":{"arxiv":["1711.03588"]},"status":"public","volume":2,"date_created":"2021-12-05T23:01:49Z","month":"12","oa_version":"Published Version","type":"journal_article","date_updated":"2021-12-07T08:04:14Z","abstract":[{"text":"We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates \"almost surely\". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice. Like others, we use variant functions (a.k.a. \"super-martingales\") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.","lang":"eng"}],"_id":"10418","acknowledgement":"McIver and Morgan are grateful to David Basin and the Information Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during part of which this work began. And thanks particularly to Andreas Lochbihler, who shared with us the probabilistic termination problem that led to it. They acknowledge the support of ARC grant DP140101119. Part of this work was carried out during the Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden. Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4.","year":"2017","doi":"10.1145/3158121","quality_controlled":"1","publication_identifier":{"eissn":["2475-1421"]},"conference":{"end_date":"2018-01-13","start_date":"2018-01-07","location":"Los Angeles, CA, United States","name":"POPL: Programming Languages"},"issue":"POPL","language":[{"iso":"eng"}],"article_number":"33","arxiv":1,"title":"A new proof rule for almost-sure termination","author":[{"full_name":"Mciver, Annabelle","first_name":"Annabelle","last_name":"Mciver"},{"last_name":"Morgan","first_name":"Carroll","full_name":"Morgan, Carroll"},{"last_name":"Kaminski","first_name":"Benjamin Lucien","full_name":"Kaminski, Benjamin Lucien"},{"id":"4524F760-F248-11E8-B48F-1D18A9856A87","full_name":"Katoen, Joost P","first_name":"Joost P","last_name":"Katoen"}],"day":"07","publication":"Proceedings of the ACM on Programming Languages","article_type":"original","article_processing_charge":"No","scopus_import":"1","publisher":"Association for Computing Machinery","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","department":[{"_id":"KrCh"},{"_id":"ToHe"}]}]