Smoothed Model Checking for Uncertain Continuous Time Markov Chains

TitleSmoothed Model Checking for Uncertain Continuous Time Markov Chains
Publication TypeReport
Year of Publication2014
AuthorsBortolussi L, Milios D, Sanguinetti G
Series TitleArXiv
Document Number1402.1450
Date Published02/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.

URLhttp://arxiv.org/abs/1402.1450
DOI