一句话：提出高效区间变点检测并与贝叶斯估计器集成，使运行时概率模型检验能应对参数突变。
近年来，概率模型检验可用于验证受参数不确定性影响的软件系统可靠性与性能属性。这类方法常用区间马尔可夫链建模，其中转移概率或速率以区间表示，并可通过带非精确先验的贝叶斯估计器在运行时持续更新。然而，贝叶斯估计器对参数真实值的突然变化反应迟缓，会产生不准确的区间，导致变化后验证结果变差。为此，论文提出一种高效的区间变化点检测方法，并将其与当前先进的带非精确先验贝叶斯估计器集成。实验表明，该端到端方法能有效处理多种参数值突变，并支持参数不确定性下的运行时概率模型检验。
Recent probabilistic model checking techniques can verify reliability and performance properties of software systems affected by parametric uncertainty. This involves modelling the system behaviour using interval Markov chains, i.e., Markov models with transition probabilities or rates specified as intervals. These intervals can be updated continually using Bayesian estimators with imprecise priors, enabling the verification of the system properties of interest at runtime. However, Bayesian estimators are slow to react to sudden changes in the actual value of the estimated parameters, yielding inaccurate intervals and leading to poor verification results after such changes. To address this limitation, we introduce an efficient interval change-point detection method, and we integrate it with a state-of-the-art Bayesian estimator with imprecise priors. Our experimental results show that the resulting end-to-end Bayesian approach to change-point detection and estimation of interval Markov chain parameters handles effectively a wide range of sudden changes in parameter values, and supports runtime probabilistic model checking under parametric uncertainty.
@inproceedings{paperbot5886,
title = {Interval change-point detection for runtime probabilistic model checking},
author = {Xingyu Zhao and Radu Calinescu and Simos Gerasimou and Valentin Robu and David Flynn},
booktitle = {ASE},
year = {2020},
doi = {10.1145/3324884.3416565}
}