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.

}, doi = {http://arxiv.org/abs/1402.1450}, url = {http://arxiv.org/abs/1402.1450}, author = {Luca Bortolussi and Dimitrios Milios and Guido Sanguinetti} }