  Smoothed model checking based on Gaussian process classification provides a
powerful approach for statistical model checking of parametric continuous time
Markov chain models. The method constructs a model for the functional
dependence of satisfaction probability on the Markov chain parameters. This is
done via Gaussian process inference methods from a limited number of
observations for different parameter combinations. In this work we consider
extensions to smoothed model checking based on sparse variational methods and
active learning. Both are used successfully to improve the scalability of
smoothed model checking. In particular, we see that active learning-based ideas
for iteratively querying the simulation model for observations can be used to
steer the model-checking to more informative areas of the parameter space and
thus improve sample efficiency. Online extensions of sparse variational
Gaussian process inference algorithms are demonstrated to provide a scalable
method for implementing active learning approaches for smoothed model checking.
