The problem
Parameter synthesis for stochastic models: finding the regions of the parameter space where a model satisfies a linear time specification with probability above (or below) a given threshold. It is a key problem for the model-based design of complex systems.
The approach
A statistical approach based on simulation, which builds on Smoothed Model Checking: a machine learning method based on Gaussian Processes for statistical parametric verification. Adding ideas from active learning gives an efficient synthesis routine that identifies the target regions with statistical guarantees.
Results
The approach, implemented in Python, scales better than existing ones with respect to the size of the model's state space and the number of parameters.