---
res:
  bibo_abstract:
  - "We consider Markov decision processes (MDPs) which are a standard model for probabilistic
    systems. We focus on qualitative properties for MDPs that can express that desired
    behaviors of the system arise almost-surely (with probability 1) or with positive
    probability.\r\nWe introduce a new simulation relation to capture the refinement
    relation of MDPs with respect to qualitative properties, and present discrete
    graph theoretic algorithms with quadratic complexity to compute the simulation
    relation.\r\nWe present an automated technique for assume-guarantee style reasoning
    for compositional analysis of MDPs with qualitative properties by giving a counter-example
    guided abstraction-refinement approach to compute our new simulation relation.
    We have implemented our algorithms and show that the compositional analysis leads
    to significant improvements. @eng"
  bibo_authorlist:
  - 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: Przemyslaw
      foaf_name: Daca, Przemyslaw
      foaf_surname: Daca
      foaf_workInfoHomepage: http://www.librecat.org/personId=49351290-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Martin
      foaf_name: Chmelik, Martin
      foaf_surname: Chmelik
      foaf_workInfoHomepage: http://www.librecat.org/personId=3624234E-F248-11E8-B48F-1D18A9856A87
  bibo_doi: 10.15479/AT:IST-2014-153-v1-1
  dct_date: 2014^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/2664-1690
  dct_language: eng
  dct_publisher: IST Austria@
  dct_title: CEGAR for qualitative analysis of probabilistic systems@
...