Earlier Version

CEGAR for qualitative analysis of probabilistic systems

K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic Systems, IST Austria, 2014.

Download
OA 423.32 KB

Technical Report | Published | English
Department
Series Title
IST Austria Technical Report
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. We 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. We 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.
Publishing Year
Date Published
2014-01-29
Page
31
ISSN
IST-REx-ID

Cite this

Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v1-1
Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v1-1
Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v1-1.
K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis of probabilistic systems. IST Austria, 2014.
Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic systems, IST Austria, 31p.
Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v1-1.
Main File(s)
File Name
Access Level
OA Open Access
Last Uploaded
2018-12-12T11:53:39Z


Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar