An approach to improve accuracy in probabilistic models using state refinement

Abstract

Probabilistic models are useful in the analysis of system be- haviour and non-functional properties. Reliable estimates and measurements of probabilities are needed to annotate behaviour models in order to generate accurate predictions. However, this may not be su cient, and may still lead to inaccurate results when the system model does not properly re ect the probabilistic choices made by the environment. Thus, not only should the probabilities be accurate in prop- erly re ecting reality, but also the model that is being used. In this paper we propose state re nement as a technique to mitigate this problem, showing that it is guaranteed to preserve or increase the accuracy of the initial model. We present a framework for iteratively improving the accuracy of a probabilistically annotated behaviour model with re- spect to a set of benchmark properties through iterative state re nements.