CEGAR for qualitative analysis of probabilistic systems Conference Paper

Author(s): Chatterjee, Krishnendu; Chmelík, Martin; Daca, Przemyslaw
Title: CEGAR for qualitative analysis of probabilistic systems
Title Series: LNCS
Affiliation IST Austria
Abstract: We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems.We focus on qualitative properties forMDPs 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 ofMDPs 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 ofMDPs with qualitative properties by giving a counterexample 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.
Conference Title: CAV: Computer Aided Verification
Volume: 8559
Conference Dates: July 18-22, 2014
Conference Location: Vienna, Austria
Publisher: Springer  
Date Published: 2014-01-01
Start Page: 473
End Page: 490
DOI: 10.1007/978-3-319-08867-9_31
Notes: A Technical Report of this paper is available at: https://repository.ist.ac.at/id/eprint/165
Open access: yes (repository)