---
res:
  bibo_abstract:
  - "Markov Decision Processes (MDPs) are a classical model for decision making in
    the presence of uncertainty. Often they are viewed as state transformers with
    planning objectives defned with respect to paths over MDP states. An increasingly\r\npopular
    alternative is to view them as distribution transformers, giving rise to a sequence
    of probability distributions over MDP states. For instance, reachability and safety
    properties in modeling robot swarms or chemical reaction networks are naturally
    defned in terms of probability distributions over states. Verifying such distributional
    properties is known to be hard and often beyond the reach of classical state-based
    verifcation techniques. In this work, we consider the problems of certifed policy
    (i.e. controller) verifcation and synthesis in MDPs under distributional reach-avoidance
    specifcations. By certifed we mean that, along with a policy, we also aim to synthesize
    a (checkable) certifcate ensuring that the MDP indeed satisfes the property. Thus,
    given the target set of distributions and an unsafe set of distributions over
    MDP states, our goal is to either synthesize a certifcate for a given policy or
    synthesize a policy along with a certifcate, proving that the target distribution
    can be reached while avoiding unsafe distributions. To solve this problem, we
    introduce the novel notion of distributional reach-avoid certifcates and present
    automated procedures for (1) synthesizing a certifcate for a given policy, and
    (2) synthesizing a policy together with the certifcate, both providing formal
    guarantees on certifcate correctness. Our experimental evaluation demonstrates
    the ability of our method to solve several non-trivial examples, including a multi-agent
    robot-swarm model, to synthesize certifed policies and to certify existing policies.
    @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.24963/ijcai.2024/1
  dct_date: 2024^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/1045-0823
  - http://id.crossref.org/issn/9781956792041
  dct_language: eng
  dct_publisher: International Joint Conferences on Artificial Intelligence@
  dct_title: Certified policy verification and synthesis for MDPs under distributional
    reach-avoidance properties@
...