---
_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-09-09T12:56:00Z
day: '17'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-37709-9_5
ec_funded: 1
external_id:
  isi:
  - '001310805600005'
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'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 13966
year: '2023'
...