---
_id: '12738'
abstract:
- lang: eng
  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.
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.
article_processing_charge: No
article_type: original
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: Stefanie
  full_name: Mohr, Stefanie
  last_name: Mohr
- 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, 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>
  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.
  ista: Chatterjee K, Katoen JP, Mohr S, Weininger M, Winkler T. 2023. Stochastic
    games with lexicographic objectives. Formal Methods in System Design.
  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>.
  short: K. Chatterjee, J.P. Katoen, S. Mohr, M. Weininger, T. Winkler, Formal Methods
    in System Design (2023).
date_created: 2023-03-19T23:00:59Z
date_published: 2023-03-08T00:00:00Z
date_updated: 2025-07-14T09:10:14Z
day: '08'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/s10703-023-00411-4
ec_funded: 1
external_id:
  isi:
  - '000946174300001'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1007/s10703-023-00411-4
month: '03'
oa: 1
oa_version: Published Version
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: Formal Methods in System Design
publication_identifier:
  eissn:
  - 1572-8102
publication_status: epub_ahead
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '8272'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Stochastic games with lexicographic 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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2023'
...
---
_id: '9393'
abstract:
- lang: eng
  text: "We consider the core algorithmic problems related to verification of systems
    with respect to three classical quantitative properties, namely, the mean-payoff,
    the ratio, and the minimum initial credit for energy property. The algorithmic
    problem given a graph and a quantitative property asks to compute the optimal
    value (the infimum value over all traces) from every node of the graph. We consider
    graphs with bounded treewidth—a class that contains the control flow graphs of
    most programs. Let n denote the number of nodes of a graph, m the number of edges
    (for bounded treewidth \U0001D45A=\U0001D442(\U0001D45B)) and W the largest absolute
    value of the weights. Our main theoretical results are as follows. First, for
    the minimum initial credit problem we show that (1) for general graphs the problem
    can be solved in \U0001D442(\U0001D45B2⋅\U0001D45A) time and the associated decision
    problem in \U0001D442(\U0001D45B⋅\U0001D45A) time, improving the previous known
    \U0001D442(\U0001D45B3⋅\U0001D45A⋅log(\U0001D45B⋅\U0001D44A)) and \U0001D442(\U0001D45B2⋅\U0001D45A)
    bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm
    that requires \U0001D442(\U0001D45B⋅log\U0001D45B) time. Second, for bounded treewidth
    graphs we present an algorithm that approximates the mean-payoff value within
    a factor of 1+\U0001D716 in time \U0001D442(\U0001D45B⋅log(\U0001D45B/\U0001D716))
    as compared to the classical exact algorithms on general graphs that require quadratic
    time. Third, for the ratio property we present an algorithm that for bounded treewidth
    graphs works in time \U0001D442(\U0001D45B⋅log(|\U0001D44E⋅\U0001D44F|))=\U0001D442(\U0001D45B⋅log(\U0001D45B⋅\U0001D44A)),
    when the output is \U0001D44E\U0001D44F, as compared to the previously best known
    algorithm on general graphs with running time \U0001D442(\U0001D45B2⋅log(\U0001D45B⋅\U0001D44A)).
    We have implemented some of our algorithms and show that they present a significant
    speedup on standard benchmarks."
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
  Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start Grant
  (279307: Graph Games), and Microsoft faculty fellows award.'
article_processing_charge: No
article_type: original
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: Rasmus
  full_name: Ibsen-Jensen, Rasmus
  id: 3B699956-F248-11E8-B48F-1D18A9856A87
  last_name: Ibsen-Jensen
  orcid: 0000-0003-4783-0389
- first_name: Andreas
  full_name: Pavlogiannis, Andreas
  id: 49704004-F248-11E8-B48F-1D18A9856A87
  last_name: Pavlogiannis
  orcid: 0000-0002-8943-0722
citation:
  ama: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative
    verification in bounded treewidth graphs. <i>Formal Methods in System Design</i>.
    2021;57:401-428. doi:<a href="https://doi.org/10.1007/s10703-021-00373-5">10.1007/s10703-021-00373-5</a>
  apa: Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2021). Faster algorithms
    for quantitative verification in bounded treewidth graphs. <i>Formal Methods in
    System Design</i>. Springer. <a href="https://doi.org/10.1007/s10703-021-00373-5">https://doi.org/10.1007/s10703-021-00373-5</a>
  chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
    “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.”
    <i>Formal Methods in System Design</i>. Springer, 2021. <a href="https://doi.org/10.1007/s10703-021-00373-5">https://doi.org/10.1007/s10703-021-00373-5</a>.
  ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for
    quantitative verification in bounded treewidth graphs,” <i>Formal Methods in System
    Design</i>, vol. 57. Springer, pp. 401–428, 2021.
  ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for
    quantitative verification in bounded treewidth graphs. Formal Methods in System
    Design. 57, 401–428.
  mla: Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification
    in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>, vol. 57,
    Springer, 2021, pp. 401–28, doi:<a href="https://doi.org/10.1007/s10703-021-00373-5">10.1007/s10703-021-00373-5</a>.
  short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System
    Design 57 (2021) 401–428.
date_created: 2021-05-16T22:01:47Z
date_published: 2021-09-01T00:00:00Z
date_updated: 2023-10-10T11:13:20Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/s10703-021-00373-5
ec_funded: 1
external_id:
  arxiv:
  - '1504.07384'
  isi:
  - '000645490300001'
intvolume: '        57'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1504.07384
month: '09'
oa: 1
oa_version: Preprint
page: 401-428
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: Formal Methods in System Design
publication_identifier:
  eissn:
  - 1572-8102
  issn:
  - 0925-9856
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster algorithms for quantitative verification in bounded treewidth graphs
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 57
year: '2021'
...