Towards accurate probabilistic models using state refinement

Abstract

Probabilistic models are useful in the analysis of system behaviour 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 sufficient, and may still lead to inaccurate results when the system model does not properly reflect the probabilistic choices made by the environment. Thus, not only should the probabilities be accurate in properly reflecting reality, but also the model that is being used. In this paper we identify and illustrate this problem showing that it can lead to inaccuracies and both false positive and false negative property checks. We propose state refinement as a technique to mitigate this problem, and present a framework for iteratively improving the accuracy of a probabilistically annotated behaviour model.