论文标题
基于采样的验证CTMC的速率不确定
Sampling-Based Verification of CTMCs with Uncertain Rates
论文作者
论文摘要
我们使用具有参数过渡速率的不确定参数CTMC和参数值的先验。先前的编码实际过渡速率的不确定性，而参数允许在过渡速率之间进行依赖。然后从先前分布中采样参数值，然后产生标准的CTMC，为此我们可以计算相关的可及性概率。我们根据以下问题提供了一种基于称为方案优化的技术的原则性解决方案：从有限的参数样本和用户指定的置信度级别，对可达性概率进行计算预测区域。预测区域应（概率很高）包含由任何其他样本引起的CTMC的可及性概率。为了提高方法的可扩展性，我们采用标准抽象技术并适应我们的方法来支持近似可及性概率。具有各种众所周知的基准的实验显示了该方法的适用性。
We employ uncertain parametric CTMCs with parametric transition rates and a prior on the parameter values. The prior encodes uncertainty about the actual transition rates, while the parameters allow dependencies between transition rates. Sampling the parameter values from the prior distribution then yields a standard CTMC, for which we may compute relevant reachability probabilities. We provide a principled solution, based on a technique called scenario-optimization, to the following problem: From a finite set of parameter samples and a user-specified confidence level, compute prediction regions on the reachability probabilities. The prediction regions should (with high probability) contain the reachability probabilities of a CTMC induced by any additional sample. To boost the scalability of the approach, we employ standard abstraction techniques and adapt our methodology to support approximate reachability probabilities. Experiments with various well-known benchmarks show the applicability of the approach.
