CEGAR for compositional analysis of qualitative properties in Markov decision processes Journal Article


Author(s): Chatterjee, Krishnendu; Chmelík, Martin; Daca, Przemysław
Article Title: CEGAR for compositional analysis of qualitative properties in Markov decision processes
Affiliation IST Austria
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 algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of two-player games by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We show a tight link between two-player games and MDPs, and as a consequence the results for games are lifted to MDPs with qualitative properties. We have implemented our algorithms and show that the compositional analysis leads to significant improvements.
Keywords: games; CEGAR; Probabilistic systems; ATL and ATL*; Simulation and alternating simulation
Journal Title: Formal Methods in System Design
Volume: 47
Issue 2
ISSN: 0925-9856
Publisher: Springer  
Date Published: 2015-10-01
Start Page: 230
End Page: 264
URL:
DOI: 10.1007/s10703-015-0235-2
Notes: The research was partly supported by Austrian Science Fund (FWF) Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE), and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).
Open access: yes (repository)
IST Austria Authors
  1. Martin Chmelik
    23 Chmelik
  2. Przemysław, Daca
    12 Daca
Related IST Austria Work