Smoothed Model Checking for Uncertain Continuous Time Markov Chains
Title | Smoothed Model Checking for Uncertain Continuous Time Markov Chains |
Publication Type | Report |
Year of Publication | 2014 |
Authors | Bortolussi L, Milios D, Sanguinetti G |
Series Title | ArXiv |
Document Number | 1402.1450 |
Date Published | 02/2014 |
Abstract | 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. |
URL | http://arxiv.org/abs/1402.1450 |
DOI |