---
_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'
...