Presentation: Prof. Luca Bortolussie (Trieste, Italy)

Machine Learning meets Formal Verification

Abstract: We will discuss novel applications of state-of-the-art Machine Learning statistical tools to deal with uncertainty in Continuous Time Markov Chains, combining them with classic tools from formal methods, mainly Model Checking. 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.
An alternative way to deal with uncertainty is to try to eliminate it exploiting available observations of the real system modelled. As it is often easier to observe and capture qualitative properties, rather than performing precise measurements, we tackled the problem of parameter estimation from observations of truth values of temporal logic formulae.
Also in this case, Gaussian Processes and Bayesian Optimisation play a central role in the solution of this problem.
In a similar way we can 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.

Bookmark the permalink.