View article

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 propose state refinement 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 respect to a set of benchmark properties through iterative state refinements.