Projects per year
Abstract
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 language | English |
---|---|
Pages (from-to) | 38-65 |
Journal | Information and Computation |
Volume | 232 |
Early online date | 9 Oct 2013 |
DOIs | |
Publication status | Published - Nov 2013 |
Keywords
- Probabilistic verification
- Compositional verification
- Assume-guarantee reasoning
- Probabilistic automata
Fingerprint
Dive into the research topics of 'Compositional probabilistic verification through multi-objective model checking'. Together they form a unique fingerprint.Projects
- 1 Finished
-
FP7_COLLAB_HIERATIC v2
Rowe, J., Good, C. & Parker, D.
European Commission, European Commission - Management Costs
1/10/12 → 30/04/16
Project: Research