Compositional probabilistic verification through multi-objective model checking

Journal article

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 theoretica...

Expand abstract

Authors: Kwiatkowska, M; Norman, G; Parker, D; Qu, H

• Publication status: Published
• Journal: INFORMATION AND COMPUTATION
• Volume: 232
• Pages: 38-65
• Publication date: 2013-11-01
• DOI: 10.1016/j.ic.2013.10.001
• EISSN: 1090-2651
• ISSN: 0890-5401
• Language: English
• Keywords: Probabilistic verification; Probabilistic automata; Assume-guarantee reasoning; Compositional verification