Bayesian statistical parametric verification and synthesis by machine learning

We consider the problem of parametric verification, presenting a recent statistical method to perform parametric verification of linear time properties of stochastic models, estimating the satisfaction probability as a function of model or property parameters. The approach leverages Bayesian Machine Learning based on Gaussian Processes. Under mild conditions on continuity of parameters of the satisfaction probability, it can be shown that property satisfaction is a smooth function of such parameters. Gaussian Processes can effectively capture this smoothness and obtain more-accurate estimates of satisfaction probabilities by transferring information across the parameter space. We leveraged this approach to efficiently solve several tasks, like parameter synthesis, system design, counterexample generation, and requirement synthesis. In this tutorial, we will introduce the basic ideas of the approach and give an overview of the different applications.