The problem
Parametric verification of stochastic models: estimating the probability that a linear time property holds, as a function of model or property parameters.
The approach
The method relies on Bayesian machine learning with Gaussian Processes. Under mild continuity conditions, property satisfaction is a smooth function of the parameters. Gaussian Processes capture this smoothness and give more accurate estimates of satisfaction probabilities by transferring information across the parameter space.
The approach has been used to solve several tasks efficiently:
- parameter synthesis;
- system design;
- counterexample generation;
- requirement synthesis.
This paper
A tutorial that introduces the basic ideas of the approach.