---
_id: '8272'
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.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Joost P
  full_name: Katoen, Joost P
  id: 4524F760-F248-11E8-B48F-1D18A9856A87
  last_name: Katoen
- first_name: Maximilian
  full_name: Weininger, Maximilian
  last_name: Weininger
- first_name: Tobias
  full_name: Winkler, Tobias
  last_name: Winkler
citation:
  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>'
  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>
  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>.
  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.
  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.'
  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>.
  short: K. Chatterjee, J.P. Katoen, M. Weininger, T. Winkler, in:, International
    Conference on Computer Aided Verification, Springer Nature, 2020, pp. 398–420.
conference:
  name: 'CAV: Computer Aided Verification'
date_created: 2020-08-16T22:00:58Z
date_published: 2020-07-14T00:00:00Z
date_updated: 2025-07-14T09:10:14Z
day: '14'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-030-53291-8_21
ec_funded: 1
external_id:
  arxiv:
  - '2005.04018'
  isi:
  - '000695272500021'
file:
- access_level: open_access
  checksum: 093d4788d7d5b2ce0ffe64fbe7820043
  content_type: application/pdf
  creator: dernst
  date_created: 2020-08-17T11:32:44Z
  date_updated: 2020-08-17T11:32:44Z
  file_id: '8276'
  file_name: 2020_LNCS_CAV_Chatterjee.pdf
  file_size: 625056
  relation: main_file
  success: 1
file_date_updated: 2020-08-17T11:32:44Z
has_accepted_license: '1'
intvolume: '     12225'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 398-420
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
publication: International Conference on Computer Aided Verification
publication_identifier:
  eissn:
  - '16113349'
  isbn:
  - '9783030532901'
  issn:
  - '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '12738'
    relation: later_version
    status: public
scopus_import: '1'
status: public
title: Stochastic games with lexicographic reachability-safety objectives
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 12225
year: '2020'
...