article published yes Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Joost P Katoen author 4524F760-F248-11E8-B48F-1D18A9856A870000-0002-6143-1926 Stefanie Mohr author Maximilian Weininger author Tobias Winkler author KrCh department Formal Methods for Stochastic Models: Algorithms and Applications project Efficient Algorithms for Computer Aided Verification project 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. https://research-explorer.ista.ac.at/download/12738/18781/2024_FromMethodsSys_Chatterjee.pdf application/pdfno Springer Nature2024 eng 1572-8102 00094617430000110.1007/s10703-023-00411-4 6340-80 https://research-explorer.ista.ac.at/record/8272 Chatterjee, Krishnendu, et al. “Stochastic Games with Lexicographic Objectives.” <i>Formal Methods in System Design</i>, vol. 63, Springer Nature, 2024, pp. 40–80, doi:<a href="https://doi.org/10.1007/s10703-023-00411-4">10.1007/s10703-023-00411-4</a>. K. Chatterjee, J. P. Katoen, S. Mohr, M. Weininger, and T. Winkler, “Stochastic games with lexicographic objectives,” <i>Formal Methods in System Design</i>, vol. 63. Springer Nature, pp. 40–80, 2024. Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. Stochastic games with lexicographic objectives. <i>Formal Methods in System Design</i>. 2024;63:40-80. doi:<a href="https://doi.org/10.1007/s10703-023-00411-4">10.1007/s10703-023-00411-4</a> K. Chatterjee, J.P. Katoen, S. Mohr, M. Weininger, T. Winkler, Formal Methods in System Design 63 (2024) 40–80. Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. 2024. Stochastic games with lexicographic objectives. Formal Methods in System Design. 63, 40–80. 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, 2024. <a href="https://doi.org/10.1007/s10703-023-00411-4">https://doi.org/10.1007/s10703-023-00411-4</a>. Chatterjee, K., Katoen, J. P., Mohr, S., Weininger, M., &#38; Winkler, T. (2024). 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> 127382023-03-19T23:00:59Z2026-04-16T09:31:13Z