Speaker : Luca Bortolussi, dipartimento di Matematica e Geoscienze, univ. di Trieste, CNR-ISTI, Pisa, Modelling and Simulation Group, Saarland university.
Title : U-check: statistical model checking under uncertainty
I will present a novel tool, U-check, that performs statistical model checking of uncertain Continuous Time Markov Chains. The focus will be mostly on the theoretical ideas underpinning it, which are based on combining state-of-the-art Machine Learning statistical tools with verification.
Uncertain CTMC are Markov Chains whose rates depend on some fixed parameter, whose precise value is unknown, but is assumed to lie in a bounded interval. The first problem we face is how to estimate the satisfaction probability of a linear temporal logic property under such uncertainty. We will show how we can reconstruct the functional dependency of the satisfaction probability on unknown parameters using Machine Learning techniques based on Gaussian Processes, which offer a flexible framework for regression and classification. We dubbed this approach Smoothed Model Checking.

Exploiting  Gaussian Processes and Bayesian Optimisation, the tool can also tackle the related problem of system design, which consists in finding optimal parameter values to enforce a certain behaviour. Again, we consider behaviours specified as linear temporal properties, combining Bayesian Optimisation with quantitative semantics.