Machine Learning Methods for Model Checking in Continuous Time Markov Chains

Model checking of temporal properties on stochastic processes is one of the major success stories of formal modelling.  The applicability of model checking methods has been greatly extended by the availability of randomized, statistical algorithms such as Statistical Model Checking (SMC).  Nevertheless, all of these methods require that a model is specified quantitatively, including a parametrization of the transition rates.  Such prior knowledge is often unavailable in many important application fields such as systems biology.  In this talk, I will discuss how an SMC procedure can be defined also for models with uncertain rates, by formalising the task in Bayesian framework and placing a non-parametric prior distribution over how the satisfaction probability of a formula depends on the model parameters.  I will introduce the notion of Gaussian Process, and show how machine learning ideas can be used also for parameter synthesys and model design.  If time permits, I'll also show how similar ideas can be used in more general reachability problems.

References:

L.Bortolussi and G. Sanguinetti, Smoothed Model Checking of Uncertain Continuous Time Markov Chains, arxiv:1402.1450

L.Bortolussi and G.Sanguinetti, Learning and Designing Stochastic Processes from Logical Constraints, QEST 2013.

L.Bortolussi and G.Sanguinetti, A statistical approach for computing reachability of non-linear and stochastic dynamical systems, QEST 2014.