---
_id: '5414'
abstract:
- lang: eng
  text: "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. "
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Przemyslaw
  full_name: Daca, Przemyslaw
  id: 49351290-F248-11E8-B48F-1D18A9856A87
  last_name: Daca
- first_name: Martin
  full_name: Chmelik, Martin
  id: 3624234E-F248-11E8-B48F-1D18A9856A87
  last_name: Chmelik
citation:
  ama: Chatterjee K, Daca P, Chmelik M. <i>CEGAR for Qualitative Analysis of Probabilistic
    Systems</i>. IST Austria; 2014. doi:<a href="https://doi.org/10.15479/AT:IST-2014-153-v3-1">10.15479/AT:IST-2014-153-v3-1</a>
  apa: Chatterjee, K., Daca, P., &#38; Chmelik, M. (2014). <i>CEGAR for qualitative
    analysis of probabilistic systems</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2014-153-v3-1">https://doi.org/10.15479/AT:IST-2014-153-v3-1</a>
  chicago: Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. <i>CEGAR for
    Qualitative Analysis of Probabilistic Systems</i>. IST Austria, 2014. <a href="https://doi.org/10.15479/AT:IST-2014-153-v3-1">https://doi.org/10.15479/AT:IST-2014-153-v3-1</a>.
  ieee: K. Chatterjee, P. Daca, and M. Chmelik, <i>CEGAR for qualitative analysis
    of probabilistic systems</i>. IST Austria, 2014.
  ista: Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic
    systems, IST Austria, 33p.
  mla: Chatterjee, Krishnendu, et al. <i>CEGAR for Qualitative Analysis of Probabilistic
    Systems</i>. IST Austria, 2014, doi:<a href="https://doi.org/10.15479/AT:IST-2014-153-v3-1">10.15479/AT:IST-2014-153-v3-1</a>.
  short: K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic
    Systems, IST Austria, 2014.
date_created: 2018-12-12T11:39:12Z
date_published: 2014-02-07T00:00:00Z
date_updated: 2025-04-15T07:56:48Z
day: '07'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2014-153-v3-1
file:
- access_level: open_access
  checksum: 87b93fe9af71fc5c94b0eb6151537e11
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:03Z
  date_updated: 2020-07-14T12:46:48Z
  file_id: '5464'
  file_name: IST-2014-153-v3+1_main.pdf
  file_size: 606227
  relation: main_file
file_date_updated: 2020-07-14T12:46:48Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '33'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '165'
related_material:
  record:
  - id: '5412'
    relation: earlier_version
    status: public
  - id: '5413'
    relation: earlier_version
    status: public
  - id: '2063'
    relation: later_version
    status: public
status: public
title: CEGAR for qualitative analysis of probabilistic systems
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...