Quantitative refinement and model checking for the analysis of probabilistic systems

Abstract

For standard (ie non-probabilistic) systems of reasonable size, correctness is analysed by simulation and/or model checking, possibly with standard program-logical arguments beforehand to reduce the problem size by abstraction. For probabilistic systems there are model checkers and simulators too; but probabilistic program logics are rarer. Thus e.g. model checkers face more severe exposure to state explosion because "front-end" probabilistic abstraction techniques are not so widely known [18]. We formalise probabilistic refinement of action systems [3] in order to provide just such a front end, and we illustrate with the probabilistic model checker PRISM [21] how it can be used to reduce state explosion. The case study is based on a performance analysis of randomised backoff in wireless communication [1]. © Springer-Verlag Berlin Heidelberg 2006.