Parametric verification of linear temporal properties for stochastic models can be expressed as computing the satisfaction probability of a certain property as a function of the parameters of the model. Smoothed model checking (smMC) aims at inferring the satisfaction function over the entire parameter space from a limited set of observations obtained via simulation. As observations are costly and noisy, smMC is framed as a Bayesian inference problem so that the estimates have an additional quantification of the uncertainty. In smMC the authors use Gaussian Processes (GP), inferred by means of the Expectation Propagation algorithm. This approach provides accurate reconstructions with statistically sound quantification of the uncertainty. However, it inherits the well-known scalability issues of GP. In this paper, we exploit recent advances in probabilistic machine learning to push this limitation forward, making Bayesian inference of smMC scalable to larger datasets and enabling its application to models with high dimensional parameter spaces. We propose Stochastic Variational Smoothed Model Checking (SV-smMC), a solution that exploits stochastic variational inference (SVI) to approximate the posterior distribution of the smMC problem. The strength and flexibility of SVI make SV-smMC applicable to two alternative probabilistic models: Gaussian Processes (GP) and Bayesian Neural Networks (BNN). The core ingredient of SVI is a stochastic gradient-based optimization that makes inference easily parallelizable and that enables GPU acceleration. In this paper, we compare the performances of smMC against those of SV-smMC by looking at the scalability, the computational efficiency and the accuracy of the reconstructed satisfaction function.

翻译：针对随机模型的线性时序性质参数验证问题，可表述为计算特定性质满足概率作为模型参数的函数。平滑模型检验旨在通过有限仿真观测数据，推断整个参数空间上的满足函数。由于观测数据成本高昂且存在噪声，该方法被构建为贝叶斯推断问题，使估计结果附带不确定性量化指标。现有平滑模型检验采用高斯过程，通过期望传播算法进行推断。该方法虽能提供统计不确定性量化下精确重建结果，但存在高斯过程固有的可扩展性问题。本文利用概率机器学习领域最新进展突破此局限，使平滑模型检验的贝叶斯推断可扩展至更大数据集，并适用于高维参数空间模型。我们提出随机变分平滑模型检验（SV-smMC），利用随机变分推断近似平滑模型检验问题的后验分布。SVI的强灵活性能使SV-smMC适用于两种可选概率模型：高斯过程与贝叶斯神经网络。SVI的核心是基于随机梯度的优化，该优化使推断易于并行化且支持GPU加速。本文通过可扩展性、计算效率及重建满足函数精度三个维度，对比平滑模型检验与SV-smMC的性能表现。