Projects per year
Abstract / Description of output
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 under mild conditions. This enables us to devise a novel Bayesian statistical algorithm which performs model checking simultaneously for all values of the model parameters from observations of truth values of the formula over individual runs of the model at isolated parameter values. This is achieved by exploiting the smoothness of the satisfaction function: by modelling explicitly correlations through a prior distribution over a space of smooth functions (a Gaussian Process), we can condition on observations at individual parameter values to construct an analytical approximation of the function itself. Extensive experiments on nontrivial case studies show that the approach is accurate and considerably faster than naive parameter exploration with standard statistical model checking methods.
Original language  English 

Pages (fromto)  235253 
Number of pages  19 
Journal  Information and Computation 
Volume  247 
Early online date  12 Jan 2016 
DOIs  
Publication status  Published  1 Apr 2016 
Fingerprint
Dive into the research topics of 'Smoothed model checking for uncertain ContinuousTime Markov Chains'. Together they form a unique fingerprint.Projects
 2 Finished

QUANTICOL  A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours (RTD)
1/04/13 → 31/03/17
Project: Research

MLCS  Machine learning for computational science statistical and formal modeling of biological systems
Sanguinetti, G.
1/10/12 → 30/09/17
Project: Research