The problem
Parameter verification and synthesis for stochastic systems are still hard problems, and they become even harder for large-scale systems when the goal is the satisfaction of linear temporal logic formulae.
This paper
A review of a number of techniques designed to tackle these problems. They rely on Gaussian Process (GP) regression and an efficient Bayesian optimisation algorithm.
Related work: Bayesian statistical parameter synthesis and the Winter Simulation Conference tutorial.