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.

翻译：基于高山流程分类的平滑模型检查为参数连续时间Markov链模型的统计模型检查提供了强有力的方法。该方法构建了Markov链参数满意概率功能依赖性功能模型。这通过高山流程从对不同参数组合的有限观测数中推导方法完成。在这项工作中,我们考虑根据稀少的变异方法和积极学习的方法,扩展平滑模型检查。这两种方法都成功地用于改进平滑模型检查的可缩放性。特别是,我们看到,可使用活跃的学习理念反复查询模拟模型观测,引导模型检查到参数空间中更多信息的领域,从而提高抽样效率。展示了稀少的变异高斯流程推算法的在线扩展,为平稳模型检查提供了一种可伸缩的方法,用于实施积极的学习方法。