---
res:
  bibo_abstract:
  - "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.@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: S.
      foaf_name: Akshay, S.
      foaf_surname: Akshay
  - foaf_Person:
      foaf_givenName: Krishnendu
      foaf_name: Chatterjee, Krishnendu
      foaf_surname: Chatterjee
      foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4561-241X
  - foaf_Person:
      foaf_givenName: Tobias
      foaf_name: Meggendorfer, Tobias
      foaf_surname: Meggendorfer
      foaf_workInfoHomepage: http://www.librecat.org/personId=b21b0c15-30a2-11eb-80dc-f13ca25802e1
    orcid: 0000-0002-1712-2165
  - foaf_Person:
      foaf_givenName: Dorde
      foaf_name: Zikelic, Dorde
      foaf_surname: Zikelic
      foaf_workInfoHomepage: http://www.librecat.org/personId=294AA7A6-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4681-1699
  bibo_doi: 10.1007/978-3-031-37709-9_5
  bibo_volume: 13966
  dct_date: 2023^xs_gYear
  dct_identifier:
  - UT:001310805600005
  dct_isPartOf:
  - http://id.crossref.org/issn/0302-9743
  - http://id.crossref.org/issn/1611-3349
  - http://id.crossref.org/issn/9783031377082
  dct_language: eng
  dct_publisher: Springer Nature@
  dct_title: 'MDPs as distribution transformers: Affine invariant synthesis for safety
    objectives@'
...