--- 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. \r\nWe 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-v3-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@ ...