Compositional probabilistic verification through multi-objective model checking

Marta Kwiatkowska, Gethin Norman, David Parker, Hongyang Qu

Research output: Contribution to journalArticlepeer-review

20 Citations (Scopus)
181 Downloads (Pure)


Compositional approaches to verification offer a powerful means to address the challenge of scalability. In this paper, we develop techniques for compositional verification of probabilistic systems based on the assume-guarantee paradigm. We target systems that exhibit both nondeterministic and stochastic behaviour, modelled as probabilistic automata, and augment these models with costs or rewards to reason about, for example, energy usage or performance metrics. Despite significant theoretical advances in compositional reasoning for probabilistic automata, there has been a distinct lack of practical progress regarding automated verification. We propose a new assume-guarantee framework based on multi-objective probabilistic model checking which supports compositional verification for a range of quantitative properties, including probabilistic ω-regular specifications and expected total cost or reward measures. We present a wide selection of assume-guarantee proof rules, including asymmetric, circular and asynchronous variants, and also show how to obtain numerical results in a compositional fashion. Given appropriate assumptions to be used in the proof rules, our compositional verification methods are, in contrast to previously proposed approaches, efficient and fully automated. Experimental results demonstrate their practical applicability on several large case studies, including instances where conventional probabilistic verification is infeasible.
Original languageEnglish
Pages (from-to)38-65
JournalInformation and Computation
Early online date9 Oct 2013
Publication statusPublished - Nov 2013


  • Probabilistic verification
  • Compositional verification
  • Assume-guarantee reasoning
  • Probabilistic automata


Dive into the research topics of 'Compositional probabilistic verification through multi-objective model checking'. Together they form a unique fingerprint.

Cite this