---
_id: '13967'
abstract:
- lang: eng
  text: 'A classic solution technique for Markov decision processes (MDP) and stochastic
    games (SG) is value iteration (VI). Due to its good practical performance, this
    approximative approach is typically preferred over exact techniques, even though
    no practical bounds on the imprecision of the result could be given until recently.
    As a consequence, even the most used model checkers could return arbitrarily wrong
    results. Over the past decade, different works derived stopping criteria, indicating
    when the precision reaches the desired level, for various settings, in particular
    MDP with reachability, total reward, and mean payoff, and SG with reachability.In
    this paper, we provide the first stopping criteria for VI on SG with total reward
    and mean payoff, yielding the first anytime algorithms in these settings. To this
    end, we provide the solution in two flavours: First through a reduction to the
    MDP case and second directly on SG. The former is simpler and automatically utilizes
    any advances on MDP. The latter allows for more local computations, heading towards
    better practical efficiency.Our solution unifies the previously mentioned approaches
    for MDP and SG and their underlying ideas. To achieve this, we isolate objective-specific
    subroutines as well as identify objective-independent concepts. These structural
    concepts, while surprisingly simple, form the very essence of the unified solution.'
acknowledgement: This research was funded in part by DFG projects 383882557 “SUV”
  and 427755713 “GOPro”.
article_processing_charge: No
arxiv: 1
author:
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
- first_name: Tobias
  full_name: Meggendorfer, Tobias
  id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
  last_name: Meggendorfer
  orcid: 0000-0002-1712-2165
- first_name: Maximilian
  full_name: Weininger, Maximilian
  id: 02ab0197-cc70-11ed-ab61-918e71f56881
  last_name: Weininger
citation:
  ama: 'Kretinsky J, Meggendorfer T, Weininger M. Stopping criteria for value iteration
    on stochastic games with quantitative objectives. In: <i>38th Annual ACM/IEEE
    Symposium on Logic in Computer Science</i>. Vol 2023. Institute of Electrical
    and Electronics Engineers; 2023. doi:<a href="https://doi.org/10.1109/LICS56636.2023.10175771">10.1109/LICS56636.2023.10175771</a>'
  apa: 'Kretinsky, J., Meggendorfer, T., &#38; Weininger, M. (2023). Stopping criteria
    for value iteration on stochastic games with quantitative objectives. In <i>38th
    Annual ACM/IEEE Symposium on Logic in Computer Science</i> (Vol. 2023). Boston,
    MA, United States: Institute of Electrical and Electronics Engineers. <a href="https://doi.org/10.1109/LICS56636.2023.10175771">https://doi.org/10.1109/LICS56636.2023.10175771</a>'
  chicago: Kretinsky, Jan, Tobias Meggendorfer, and Maximilian Weininger. “Stopping
    Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.”
    In <i>38th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Vol. 2023.
    Institute of Electrical and Electronics Engineers, 2023. <a href="https://doi.org/10.1109/LICS56636.2023.10175771">https://doi.org/10.1109/LICS56636.2023.10175771</a>.
  ieee: J. Kretinsky, T. Meggendorfer, and M. Weininger, “Stopping criteria for value
    iteration on stochastic games with quantitative objectives,” in <i>38th Annual
    ACM/IEEE Symposium on Logic in Computer Science</i>, Boston, MA, United States,
    2023, vol. 2023.
  ista: 'Kretinsky J, Meggendorfer T, Weininger M. 2023. Stopping criteria for value
    iteration on stochastic games with quantitative objectives. 38th Annual ACM/IEEE
    Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science
    vol. 2023.'
  mla: Kretinsky, Jan, et al. “Stopping Criteria for Value Iteration on Stochastic
    Games with Quantitative Objectives.” <i>38th Annual ACM/IEEE Symposium on Logic
    in Computer Science</i>, vol. 2023, Institute of Electrical and Electronics Engineers,
    2023, doi:<a href="https://doi.org/10.1109/LICS56636.2023.10175771">10.1109/LICS56636.2023.10175771</a>.
  short: J. Kretinsky, T. Meggendorfer, M. Weininger, in:, 38th Annual ACM/IEEE Symposium
    on Logic in Computer Science, Institute of Electrical and Electronics Engineers,
    2023.
conference:
  end_date: 2023-06-29
  location: Boston, MA, United States
  name: 'LICS: Symposium on Logic in Computer Science'
  start_date: 2023-06-26
date_created: 2023-08-06T22:01:10Z
date_published: 2023-07-01T00:00:00Z
date_updated: 2023-12-13T12:06:10Z
day: '01'
department:
- _id: KrCh
doi: 10.1109/LICS56636.2023.10175771
external_id:
  arxiv:
  - '2304.09930'
  isi:
  - '001036707700042'
intvolume: '      2023'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.48550/arXiv.2304.09930
month: '07'
oa: 1
oa_version: Preprint
publication: 38th Annual ACM/IEEE Symposium on Logic in Computer Science
publication_identifier:
  isbn:
  - '9798350335873'
  issn:
  - 1043-6871
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
scopus_import: '1'
status: public
title: Stopping criteria for value iteration on stochastic games with quantitative
  objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 2023
year: '2023'
...
---
_id: '10002'
abstract:
- lang: eng
  text: 'We present a faster symbolic algorithm for the following central problem
    in probabilistic verification: Compute the maximal end-component (MEC) decomposition
    of Markov decision processes (MDPs). This problem generalizes the SCC decomposition
    problem of graphs and closed recurrent sets of Markov chains. The model of symbolic
    algorithms is widely used in formal verification and model-checking, where access
    to the input model is restricted to only symbolic operations (e.g., basic set
    operations and computation of one-step neighborhood). For an input MDP with  n  vertices
    and  m  edges, the classical symbolic algorithm from the 1990s for the MEC decomposition
    requires  O(n2)  symbolic operations and  O(1)  symbolic space. The only other
    symbolic algorithm for the MEC decomposition requires  O(nm−−√)  symbolic operations
    and  O(m−−√)  symbolic space. A main open question is whether the worst-case  O(n2)  bound
    for symbolic operations can be beaten. We present a symbolic algorithm that requires  O˜(n1.5)  symbolic
    operations and  O˜(n−−√)  symbolic space. Moreover, the parametrization of our
    algorithm provides a trade-off between symbolic operations and symbolic space:
    for all  0<ϵ≤1/2  the symbolic algorithm requires  O˜(n2−ϵ)  symbolic operations
    and  O˜(nϵ)  symbolic space ( O˜  hides poly-logarithmic factors). Using our techniques
    we present faster algorithms for computing the almost-sure winning regions of  ω
    -regular objectives for MDPs. We consider the canonical parity objectives for  ω
    -regular objectives, and for parity objectives with  d -priorities we present
    an algorithm that computes the almost-sure winning region with  O˜(n2−ϵ)  symbolic
    operations and  O˜(nϵ)  symbolic space, for all  0<ϵ≤1/2 .'
acknowledgement: The authors are grateful to the anonymous referees for their valuable
  comments. A. S. is fully supported by the Vienna Science and Technology Fund (WWTF)
  through project ICT15–003. K. C. is supported by the Austrian Science Fund (FWF)
  NFN Grant No S11407-N23 (RiSE/SHiNE) and by the ERC CoG 863818 (ForM-SMArt). For
  M. H. the research leading to these results has received funding from the European
  Research Council under the European Unions Seventh Framework Programme (FP/2007–2013)
  / ERC Grant Agreement no. 340506.
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: Wolfgang
  full_name: Dvorak, Wolfgang
  last_name: Dvorak
- first_name: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
- first_name: Alexander
  full_name: Svozil, Alexander
  last_name: Svozil
citation:
  ama: 'Chatterjee K, Dvorak W, Henzinger MH, Svozil A. Symbolic time and space tradeoffs
    for probabilistic verification. In: <i>Proceedings of the 36th Annual ACM/IEEE
    Symposium on Logic in Computer Science</i>. Institute of Electrical and Electronics
    Engineers; 2021:1-13. doi:<a href="https://doi.org/10.1109/LICS52264.2021.9470739">10.1109/LICS52264.2021.9470739</a>'
  apa: 'Chatterjee, K., Dvorak, W., Henzinger, M. H., &#38; Svozil, A. (2021). Symbolic
    time and space tradeoffs for probabilistic verification. In <i>Proceedings of
    the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 1–13).
    Rome, Italy: Institute of Electrical and Electronics Engineers. <a href="https://doi.org/10.1109/LICS52264.2021.9470739">https://doi.org/10.1109/LICS52264.2021.9470739</a>'
  chicago: Chatterjee, Krishnendu, Wolfgang Dvorak, Monika H Henzinger, and Alexander
    Svozil. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” In
    <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>,
    1–13. Institute of Electrical and Electronics Engineers, 2021. <a href="https://doi.org/10.1109/LICS52264.2021.9470739">https://doi.org/10.1109/LICS52264.2021.9470739</a>.
  ieee: K. Chatterjee, W. Dvorak, M. H. Henzinger, and A. Svozil, “Symbolic time and
    space tradeoffs for probabilistic verification,” in <i>Proceedings of the 36th
    Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Rome, Italy, 2021,
    pp. 1–13.
  ista: 'Chatterjee K, Dvorak W, Henzinger MH, Svozil A. 2021. Symbolic time and space
    tradeoffs for probabilistic verification. Proceedings of the 36th Annual ACM/IEEE
    Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science,
    1–13.'
  mla: Chatterjee, Krishnendu, et al. “Symbolic Time and Space Tradeoffs for Probabilistic
    Verification.” <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in
    Computer Science</i>, Institute of Electrical and Electronics Engineers, 2021,
    pp. 1–13, doi:<a href="https://doi.org/10.1109/LICS52264.2021.9470739">10.1109/LICS52264.2021.9470739</a>.
  short: K. Chatterjee, W. Dvorak, M.H. Henzinger, A. Svozil, in:, Proceedings of
    the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of
    Electrical and Electronics Engineers, 2021, pp. 1–13.
conference:
  end_date: 2021-07-02
  location: Rome, Italy
  name: 'LICS: Symposium on Logic in Computer Science'
  start_date: 2021-06-29
date_created: 2021-09-12T22:01:24Z
date_published: 2021-07-07T00:00:00Z
date_updated: 2025-07-14T09:10:07Z
day: '07'
department:
- _id: KrCh
doi: 10.1109/LICS52264.2021.9470739
ec_funded: 1
external_id:
  arxiv:
  - '2104.07466'
  isi:
  - '000947350400089'
isi: 1
keyword:
- Computer science
- Computational modeling
- Markov processes
- Probabilistic logic
- Formal verification
- Game Theory
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/2104.07466
month: '07'
oa: 1
oa_version: Preprint
page: 1-13
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer
  Science
publication_identifier:
  eisbn:
  - 978-1-6654-4895-6
  isbn:
  - 978-1-6654-4896-3
  issn:
  - 1043-6871
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic time and space tradeoffs for probabilistic verification
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '10004'
abstract:
- lang: eng
  text: 'Markov chains are the de facto finite-state model for stochastic dynamical
    systems, and Markov decision processes (MDPs) extend Markov chains by incorporating
    non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization
    criterion is the maximal expected total reward where the MDP stops after T steps,
    which can be computed by a simple dynamic programming algorithm. We consider a
    natural generalization of the problem where the stopping times can be chosen according
    to a probability distribution, such that the expected stopping time is T, to optimize
    the expected total reward. Quite surprisingly we establish inter-reducibility
    of the expected stopping-time problem for Markov chains with the Positivity problem
    (which is related to the well-known Skolem problem), for which establishing either
    decidability or undecidability would be a major breakthrough. Given the hardness
    of the exact problem, we consider the approximate version of the problem: we show
    that it can be solved in exponential time for Markov chains and in exponential
    space for MDPs.'
acknowledgement: We are grateful to the anonymous reviewers of LICS 2021 and of a
  previous version of this paper for insightful comments that helped improving the
  presentation. This research was partially supported by the grant ERC CoG 863818
  (ForM-SMArt).
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: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
citation:
  ama: 'Chatterjee K, Doyen L. Stochastic processes with expected stopping time. In:
    <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>.
    Institute of Electrical and Electronics Engineers; 2021:1-13. doi:<a href="https://doi.org/10.1109/LICS52264.2021.9470595">10.1109/LICS52264.2021.9470595</a>'
  apa: 'Chatterjee, K., &#38; Doyen, L. (2021). Stochastic processes with expected
    stopping time. In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic
    in Computer Science</i> (pp. 1–13). Rome, Italy: Institute of Electrical and Electronics
    Engineers. <a href="https://doi.org/10.1109/LICS52264.2021.9470595">https://doi.org/10.1109/LICS52264.2021.9470595</a>'
  chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected
    Stopping Time.” In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic
    in Computer Science</i>, 1–13. Institute of Electrical and Electronics Engineers,
    2021. <a href="https://doi.org/10.1109/LICS52264.2021.9470595">https://doi.org/10.1109/LICS52264.2021.9470595</a>.
  ieee: K. Chatterjee and L. Doyen, “Stochastic processes with expected stopping time,”
    in <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>,
    Rome, Italy, 2021, pp. 1–13.
  ista: 'Chatterjee K, Doyen L. 2021. Stochastic processes with expected stopping
    time. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science.
    LICS: Symposium on Logic in Computer Science, 1–13.'
  mla: Chatterjee, Krishnendu, and Laurent Doyen. “Stochastic Processes with Expected
    Stopping Time.” <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic
    in Computer Science</i>, Institute of Electrical and Electronics Engineers, 2021,
    pp. 1–13, doi:<a href="https://doi.org/10.1109/LICS52264.2021.9470595">10.1109/LICS52264.2021.9470595</a>.
  short: K. Chatterjee, L. Doyen, in:, Proceedings of the 36th Annual ACM/IEEE Symposium
    on Logic in Computer Science, Institute of Electrical and Electronics Engineers,
    2021, pp. 1–13.
conference:
  end_date: 2021-07-02
  location: Rome, Italy
  name: 'LICS: Symposium on Logic in Computer Science'
  start_date: 2021-06-29
date_created: 2021-09-12T22:01:25Z
date_published: 2021-07-07T00:00:00Z
date_updated: 2025-07-14T09:10:08Z
day: '07'
department:
- _id: KrCh
doi: 10.1109/LICS52264.2021.9470595
ec_funded: 1
external_id:
  arxiv:
  - '2104.07278'
  isi:
  - '000947350400036'
isi: 1
keyword:
- Computer science
- Heuristic algorithms
- Memory management
- Automata
- Markov processes
- Probability distribution
- Complexity theory
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/2104.07278
month: '07'
oa: 1
oa_version: Preprint
page: 1-13
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer
  Science
publication_identifier:
  eisbn:
  - 978-1-6654-4895-6
  isbn:
  - 978-1-6654-4896-3
  issn:
  - 1043-6871
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
scopus_import: '1'
status: public
title: Stochastic processes with expected stopping time
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '4519'
abstract:
- lang: eng
  text: We summarize several recent results about hybrid automata. Our goal is to
    demonstrate that concepts from the theory of discrete concurrent systems can give
    insights into partly continuous systems, and that methods for the verification
    of finite-state systems can be used to analyze certain systems with uncountable
    state spaces
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: 'Henzinger TA. The theory of hybrid automata. In: <i>Proceedings 11th Annual
    IEEE Symposium on Logic in Computer Science</i>. IEEE; 1996:278-292. doi:<a href="https://doi.org/10.1109/LICS.1996.561342
    ">10.1109/LICS.1996.561342 </a>'
  apa: 'Henzinger, T. A. (1996). The theory of hybrid automata. In <i>Proceedings
    11th Annual IEEE Symposium on Logic in Computer Science</i> (pp. 278–292). New
    Brunswick, NJ, United States of America: IEEE. <a href="https://doi.org/10.1109/LICS.1996.561342
    ">https://doi.org/10.1109/LICS.1996.561342 </a>'
  chicago: Henzinger, Thomas A. “The Theory of Hybrid Automata.” In <i>Proceedings
    11th Annual IEEE Symposium on Logic in Computer Science</i>, 278–92. IEEE, 1996.
    <a href="https://doi.org/10.1109/LICS.1996.561342 ">https://doi.org/10.1109/LICS.1996.561342
    </a>.
  ieee: T. A. Henzinger, “The theory of hybrid automata,” in <i>Proceedings 11th Annual
    IEEE Symposium on Logic in Computer Science</i>, New Brunswick, NJ, United States
    of America, 1996, pp. 278–292.
  ista: 'Henzinger TA. 1996. The theory of hybrid automata. Proceedings 11th Annual
    IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science,
    278–292.'
  mla: Henzinger, Thomas A. “The Theory of Hybrid Automata.” <i>Proceedings 11th Annual
    IEEE Symposium on Logic in Computer Science</i>, IEEE, 1996, pp. 278–92, doi:<a
    href="https://doi.org/10.1109/LICS.1996.561342 ">10.1109/LICS.1996.561342 </a>.
  short: T.A. Henzinger, in:, Proceedings 11th Annual IEEE Symposium on Logic in Computer
    Science, IEEE, 1996, pp. 278–292.
conference:
  end_date: 1996-07-30
  location: New Brunswick, NJ, United States of America
  name: 'LICS: Logic in Computer Science'
  start_date: 1996-07-27
date_created: 2018-12-11T12:09:16Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2022-07-06T07:56:28Z
day: '01'
doi: '10.1109/LICS.1996.561342 '
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://ieeexplore.ieee.org/document/561342
month: '01'
oa_version: None
page: 278 - 292
publication: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science
publication_identifier:
  issn:
  - 1043-6871
publication_status: published
publisher: IEEE
publist_id: '213'
quality_controlled: '1'
status: public
title: The theory of hybrid automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1996'
...