Smoothed Model Checking for Uncertain Continuous Time Markov Chains
|Title||Smoothed Model Checking for Uncertain Continuous Time Markov Chains|
|Year of Publication||2014|
|Authors||Bortolussi L, Milios D, Sanguinetti G|
We consider the problem of computing the satisfaction probability of a formula for stochastic models with parametric uncertainty. We show that this satisfaction probability is a smooth function of the model parameters. We then propose a novel statistical algorithm which performs statistical model checking by leveraging the smoothness of the satisfaction probability in a Bayesian hierarchical modelling framework. In this way, our approach is able to provide an analytical approximation to the satisfaction probability of a formula, yielding an estimate of the satisfaction probability at all values of the parameters from observations of truth values over a small number of individual simulations of the system. Empirical results on non-trivial case studies show that the approach is accurate and several orders of magnitude faster than standard statistical model checking methods.