---
res:
  bibo_abstract:
  - 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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Krishnendu
      foaf_name: Chatterjee, Krishnendu
      foaf_surname: Chatterjee
      foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4561-241X
  - foaf_Person:
      foaf_givenName: Joost P
      foaf_name: Katoen, Joost P
      foaf_surname: Katoen
      foaf_workInfoHomepage: http://www.librecat.org/personId=4524F760-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Stefanie
      foaf_name: Mohr, Stefanie
      foaf_surname: Mohr
  - foaf_Person:
      foaf_givenName: Maximilian
      foaf_name: Weininger, Maximilian
      foaf_surname: Weininger
  - foaf_Person:
      foaf_givenName: Tobias
      foaf_name: Winkler, Tobias
      foaf_surname: Winkler
  bibo_doi: 10.1007/s10703-023-00411-4
  bibo_volume: 63
  dct_date: 2024^xs_gYear
  dct_identifier:
  - UT:000946174300001
  dct_isPartOf:
  - http://id.crossref.org/issn/1572-8102
  dct_language: eng
  dct_publisher: Springer Nature@
  dct_title: Stochastic games with lexicographic objectives@
...