thesis published Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Przemyslaw Daca author 49351290-F248-11E8-B48F-1D18A9856A87 Martin Chmelik author 3624234E-F248-11E8-B48F-1D18A9856A87 KrCh department 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. https://research-explorer.ista.ac.at/download/5412/5500/IST-2014-153-v1+1_main.pdf application/pdfno IST Austria2014 eng 2664-169010.15479/AT:IST-2014-153-v1-1 31 https://research-explorer.ista.ac.at/record/5413 https://research-explorer.ista.ac.at/record/5414 https://research-explorer.ista.ac.at/record/2063 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-v1-1">https://doi.org/10.15479/AT:IST-2014-153-v1-1</a>. K. Chatterjee, P. Daca, 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 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-v1-1">10.15479/AT:IST-2014-153-v1-1</a> 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-v1-1">10.15479/AT:IST-2014-153-v1-1</a>. 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-v1-1">https://doi.org/10.15479/AT:IST-2014-153-v1-1</a> K. Chatterjee, P. Daca, and M. Chmelik, <i>CEGAR for qualitative analysis of probabilistic systems</i>. IST Austria, 2014. 54122018-12-12T11:39:11Z2025-04-15T07:56:48Z