---
_id: '14317'
abstract:
- lang: eng
  text: "Markov decision processes can be viewed as transformers of probability distributions.
    While this view is useful from a practical standpoint to reason about trajectories
    of distributions, basic reachability and safety problems are known to be computationally
    intractable (i.e., Skolem-hard) to solve in such models. Further, we show that
    even for simple examples of MDPs, strategies for safety objectives over distributions
    can require infinite memory and randomization.\r\nIn light of this, we present
    a novel overapproximation approach to synthesize strategies in an MDP, such that
    a safety objective over the distributions is met. More precisely, we develop a
    new framework for template-based synthesis of certificates as affine distributional
    and inductive invariants for safety objectives in MDPs. We provide two algorithms
    within this framework. One can only synthesize memoryless strategies, but has
    relative completeness guarantees, while the other can synthesize general strategies.
    The runtime complexity of both algorithms is in PSPACE. We implement these algorithms
    and show that they can solve several non-trivial examples."
acknowledgement: This work was supported in part by the ERC CoG 863818 (FoRM-SMArt)
  and the European Union’s Horizon 2020 research and innovation programme under the
  Marie Skłodowska-Curie Grant Agreement No. 665385 as well as DST/CEFIPRA/INRIA project
  EQuaVE and SERB Matrices grant MTR/2018/00074.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: S.
  full_name: Akshay, S.
  last_name: Akshay
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Tobias
  full_name: Meggendorfer, Tobias
  id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
  last_name: Meggendorfer
  orcid: 0000-0002-1712-2165
- first_name: Dorde
  full_name: Zikelic, Dorde
  id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
  last_name: Zikelic
  orcid: 0000-0002-4681-1699
citation:
  ama: 'Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. MDPs as distribution transformers:
    Affine invariant synthesis for safety objectives. In: <i>International Conference
    on Computer Aided Verification</i>. Vol 13966. Springer Nature; 2023:86-112. doi:<a
    href="https://doi.org/10.1007/978-3-031-37709-9_5">10.1007/978-3-031-37709-9_5</a>'
  apa: 'Akshay, S., Chatterjee, K., Meggendorfer, T., &#38; Zikelic, D. (2023). MDPs
    as distribution transformers: Affine invariant synthesis for safety objectives.
    In <i>International Conference on Computer Aided Verification</i> (Vol. 13966,
    pp. 86–112). Paris, France: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-37709-9_5">https://doi.org/10.1007/978-3-031-37709-9_5</a>'
  chicago: 'Akshay, S., Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic.
    “MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.”
    In <i>International Conference on Computer Aided Verification</i>, 13966:86–112.
    Springer Nature, 2023. <a href="https://doi.org/10.1007/978-3-031-37709-9_5">https://doi.org/10.1007/978-3-031-37709-9_5</a>.'
  ieee: 'S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “MDPs as distribution
    transformers: Affine invariant synthesis for safety objectives,” in <i>International
    Conference on Computer Aided Verification</i>, Paris, France, 2023, vol. 13966,
    pp. 86–112.'
  ista: 'Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2023. MDPs as distribution
    transformers: Affine invariant synthesis for safety objectives. International
    Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
    vol. 13966, 86–112.'
  mla: 'Akshay, S., et al. “MDPs as Distribution Transformers: Affine Invariant Synthesis
    for Safety Objectives.” <i>International Conference on Computer Aided Verification</i>,
    vol. 13966, Springer Nature, 2023, pp. 86–112, doi:<a href="https://doi.org/10.1007/978-3-031-37709-9_5">10.1007/978-3-031-37709-9_5</a>.'
  short: S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, International
    Conference on Computer Aided Verification, Springer Nature, 2023, pp. 86–112.
conference:
  end_date: 2023-07-22
  location: Paris, France
  name: 'CAV: Computer Aided Verification'
  start_date: 2023-07-17
date_created: 2023-09-10T22:01:12Z
date_published: 2023-07-17T00:00:00Z
date_updated: 2025-07-14T09:09:56Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-37709-9_5
ec_funded: 1
file:
- access_level: open_access
  checksum: f143c8eedf609f20f2aad2eeb496d53f
  content_type: application/pdf
  creator: dernst
  date_created: 2023-09-20T08:46:43Z
  date_updated: 2023-09-20T08:46:43Z
  file_id: '14349'
  file_name: 2023_LNCS_Akshay.pdf
  file_size: 531745
  relation: main_file
  success: 1
file_date_updated: 2023-09-20T08:46:43Z
has_accepted_license: '1'
intvolume: '     13966'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 86-112
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
  call_identifier: H2020
  grant_number: '665385'
  name: International IST Doctoral Program
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: International Conference on Computer Aided Verification
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783031377082'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'MDPs as distribution transformers: Affine invariant synthesis for 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13966
year: '2023'
...
---
_id: '14318'
abstract:
- lang: eng
  text: "Probabilistic recurrence relations (PRRs) are a standard formalism for describing
    the runtime of a randomized algorithm. Given a PRR and a time limit κ, we consider
    the tail probability Pr[T≥κ], i.e., the probability that the randomized runtime
    T of the PRR exceeds κ. Our focus is the formal analysis of tail bounds that aims
    at finding a tight asymptotic upper bound u≥Pr[T≥κ]. To address this problem,
    the classical and most well-known approach is the cookbook method by Karp (JACM
    1994), while other approaches are mostly limited to deriving tail bounds of specific
    PRRs via involved custom analysis.\r\nIn this work, we propose a novel approach
    for deriving the common exponentially-decreasing tail bounds for PRRs whose preprocessing
    time and random passed sizes observe discrete or (piecewise) uniform distribution
    and whose recursive call is either a single procedure call or a divide-and-conquer.
    We first establish a theoretical approach via Markov’s inequality, and then instantiate
    the theoretical approach with a template-based algorithmic approach via a refined
    treatment of exponentiation. Experimental evaluation shows that our algorithmic
    approach is capable of deriving tail bounds that are (i) asymptotically tighter
    than Karp’s method, (ii) match the best-known manually-derived asymptotic tail
    bound for QuickSelect, and (iii) is only slightly worse (with a loglogn factor)
    than the manually-proven optimal asymptotic tail bound for QuickSort. Moreover,
    our algorithmic approach handles all examples (including realistic PRRs such as
    QuickSort, QuickSelect, DiameterComputation, etc.) in less than 0.1 s, showing
    that our approach is efficient in practice."
acknowledgement: We thank Prof. Bican Xia for valuable information on the exponential
  theory of reals. The work is partially supported by the National Natural Science
  Foundation of China (NSFC) with Grant No. 62172271, ERC CoG 863818 (ForM-SMArt),
  the Hong Kong Research Grants Council ECS Project Number 26208122, the HKUST-Kaisa
  Joint Research Institute Project Grant HKJRI3A-055 and the HKUST Startup Grant R9272.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Yican
  full_name: Sun, Yican
  last_name: Sun
- first_name: Hongfei
  full_name: Fu, Hongfei
  last_name: Fu
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
  full_name: Goharshady, Amir Kafshdar
  id: 391365CE-F248-11E8-B48F-1D18A9856A87
  last_name: Goharshady
  orcid: 0000-0003-1702-6584
citation:
  ama: 'Sun Y, Fu H, Chatterjee K, Goharshady AK. Automated tail bound analysis for probabilistic
    recurrence relations. In: <i>Computer Aided Verification</i>. Vol 13966. Springer
    Nature; 2023:16-39. doi:<a href="https://doi.org/10.1007/978-3-031-37709-9_2">10.1007/978-3-031-37709-9_2</a>'
  apa: 'Sun, Y., Fu, H., Chatterjee, K., &#38; Goharshady, A. K. (2023). Automated
    tail bound analysis for probabilistic recurrence relations. In <i>Computer Aided
    Verification</i> (Vol. 13966, pp. 16–39). Paris, France: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-37709-9_2">https://doi.org/10.1007/978-3-031-37709-9_2</a>'
  chicago: Sun, Yican, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady.
    “Automated Tail Bound Analysis for Probabilistic Recurrence Relations.” In <i>Computer
    Aided Verification</i>, 13966:16–39. Springer Nature, 2023. <a href="https://doi.org/10.1007/978-3-031-37709-9_2">https://doi.org/10.1007/978-3-031-37709-9_2</a>.
  ieee: Y. Sun, H. Fu, K. Chatterjee, and A. K. Goharshady, “Automated tail bound
    analysis for probabilistic recurrence relations,” in <i>Computer Aided Verification</i>,
    Paris, France, 2023, vol. 13966, pp. 16–39.
  ista: 'Sun Y, Fu H, Chatterjee K, Goharshady AK. 2023. Automated tail bound analysis
    for probabilistic recurrence relations. Computer Aided Verification. CAV: Computer
    Aided Verification, LNCS, vol. 13966, 16–39.'
  mla: Sun, Yican, et al. “Automated Tail Bound Analysis for Probabilistic Recurrence
    Relations.” <i>Computer Aided Verification</i>, vol. 13966, Springer Nature, 2023,
    pp. 16–39, doi:<a href="https://doi.org/10.1007/978-3-031-37709-9_2">10.1007/978-3-031-37709-9_2</a>.
  short: Y. Sun, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Computer Aided Verification,
    Springer Nature, 2023, pp. 16–39.
conference:
  end_date: 2023-07-22
  location: Paris, France
  name: 'CAV: Computer Aided Verification'
  start_date: 2023-07-17
date_created: 2023-09-10T22:01:12Z
date_published: 2023-07-17T00:00:00Z
date_updated: 2025-07-14T09:09:57Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-37709-9_2
ec_funded: 1
file:
- access_level: open_access
  checksum: 42917e086f8c7699f3bccf84f74fe000
  content_type: application/pdf
  creator: dernst
  date_created: 2023-09-20T08:24:47Z
  date_updated: 2023-09-20T08:24:47Z
  file_id: '14348'
  file_name: 2023_LNCS_Sun.pdf
  file_size: 624647
  relation: main_file
  success: 1
file_date_updated: 2023-09-20T08:24:47Z
has_accepted_license: '1'
intvolume: '     13966'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 16-39
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Computer Aided Verification
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783031377082'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
  link:
  - relation: software
    url: https://github.com/boyvolcano/PRR
scopus_import: '1'
status: public
title: Automated tail bound analysis for probabilistic recurrence relations
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13966
year: '2023'
...
---
_id: '14758'
abstract:
- lang: eng
  text: 'We present a flexible and efficient toolchain to symbolically solve (standard)
    Rabin games, fair-adversarial Rabin games, and 2 1/2 license type-player Rabin
    games. To our best knowledge, our tools are the first ones to be able to solve
    these problems. Furthermore, using these flexible game solvers as a back-end,
    we implemented a tool for computing correct-by-construction controllers for stochastic
    dynamical systems under LTL specifications. Our implementations use the recent
    theoretical result that all of these games can be solved using the same symbolic
    fixpoint algorithm but utilizing different, domain specific calculations of the
    involved predecessor operators. The main feature of our toolchain is the utilization
    of two programming abstractions: one to separate the symbolic fixpoint computations
    from the predecessor calculations, and another one to allow the integration of
    different BDD libraries as back-ends. In particular, we employ a multi-threaded
    execution of the fixpoint algorithm by using the multi-threaded BDD library Sylvan,
    which leads to enormous computational savings.'
acknowledgement: 'Authors ordered alphabetically. R. Majumdar and A.-K. Schmuck are
  partially supported by DFG project 389792660 TRR 248-CPEC. A.-K. Schmuck is additionally
  funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project
  ERC-2020-AdG 101020093. M. Rychlicki is supported by the EPSRC project EP/V00252X/1.
  S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802,
  and ERC 101089047.'
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Rupak
  full_name: Majumdar, Rupak
  last_name: Majumdar
- first_name: Kaushik
  full_name: Mallik, Kaushik
  id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
  last_name: Mallik
  orcid: 0000-0001-9864-7475
- first_name: Mateusz
  full_name: Rychlicki, Mateusz
  last_name: Rychlicki
- first_name: Anne-Kathrin
  full_name: Schmuck, Anne-Kathrin
  last_name: Schmuck
- first_name: Sadegh
  full_name: Soudjani, Sadegh
  last_name: Soudjani
citation:
  ama: 'Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain
    for symbolic rabin games under fair and stochastic uncertainties. In: <i>35th
    International Conference on Computer Aided Verification</i>. Vol 13966. Springer
    Nature; 2023:3-15. doi:<a href="https://doi.org/10.1007/978-3-031-37709-9_1">10.1007/978-3-031-37709-9_1</a>'
  apa: 'Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., &#38; Soudjani, S.
    (2023). A flexible toolchain for symbolic rabin games under fair and stochastic
    uncertainties. In <i>35th International Conference on Computer Aided Verification</i>
    (Vol. 13966, pp. 3–15). Paris, France: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-37709-9_1">https://doi.org/10.1007/978-3-031-37709-9_1</a>'
  chicago: Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck,
    and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair
    and Stochastic Uncertainties.” In <i>35th International Conference on Computer
    Aided Verification</i>, 13966:3–15. Springer Nature, 2023. <a href="https://doi.org/10.1007/978-3-031-37709-9_1">https://doi.org/10.1007/978-3-031-37709-9_1</a>.
  ieee: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible
    toolchain for symbolic rabin games under fair and stochastic uncertainties,” in
    <i>35th International Conference on Computer Aided Verification</i>, Paris, France,
    2023, vol. 13966, pp. 3–15.
  ista: 'Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible
    toolchain for symbolic rabin games under fair and stochastic uncertainties. 35th
    International Conference on Computer Aided Verification. CAV: Computer Aided Verification,
    LNCS, vol. 13966, 3–15.'
  mla: Majumdar, Rupak, et al. “A Flexible Toolchain for Symbolic Rabin Games under
    Fair and Stochastic Uncertainties.” <i>35th International Conference on Computer
    Aided Verification</i>, vol. 13966, Springer Nature, 2023, pp. 3–15, doi:<a href="https://doi.org/10.1007/978-3-031-37709-9_1">10.1007/978-3-031-37709-9_1</a>.
  short: R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, in:, 35th
    International Conference on Computer Aided Verification, Springer Nature, 2023,
    pp. 3–15.
conference:
  end_date: 2023-07-22
  location: Paris, France
  name: 'CAV: Computer Aided Verification'
  start_date: 2023-07-17
date_created: 2024-01-08T13:18:00Z
date_published: 2023-07-16T00:00:00Z
date_updated: 2024-02-27T07:39:51Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-37709-9_1
ec_funded: 1
file:
- access_level: open_access
  checksum: 1a361d83db0244fd32c03b544c294b5a
  content_type: application/pdf
  creator: dernst
  date_created: 2024-01-09T10:01:07Z
  date_updated: 2024-01-09T10:01:07Z
  file_id: '14765'
  file_name: 2023_LNCSCAV_Majumdar.pdf
  file_size: 405147
  relation: main_file
  success: 1
file_date_updated: 2024-01-09T10:01:07Z
has_accepted_license: '1'
intvolume: '     13966'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 3-15
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 35th International Conference on Computer Aided Verification
publication_identifier:
  eisbn:
  - '9783031377099'
  eissn:
  - 1611-3349
  isbn:
  - '9783031377082'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '14994'
    relation: research_data
    status: public
scopus_import: '1'
status: public
title: A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13966
year: '2023'
...