扰动概率系统定量验证的渐近界
Asymptotic Bounds for Quantitative Verification of Perturbed Probabilistic Systems
摘要：
大多数现有的概率模型检验案例研究是基于很好理解的理论模型和分布。然而，现实生活中的概率系统通常涉及分布参数，其值是通过经验测量获得的，因此受到小扰动。在本文中，我们考虑这些系统的参数模型（即，参数马尔可夫链）配备了绝对距离的范数。我们的主要贡献是一种方法来计算渐近界的形式的条件数的约束可达概率对扰动的分布参数的系统。通过Zeroconf协议和跳蛙问题的实验证明了该方法的有效性。
英文摘要：
The majority of existing probabilistic model checking case studies are based on well understood theoretical models and distributions. However, real-life probabilistic systems usually involve distribution parameters whose values are obtained by empirical measurements and thus are subject to small perturbations. In this paper, we consider perturbation analysis of reachability in the parametric models of these systems (i.e., parametric Markov chains) equipped with the norm of absolute distance. Our main contribution is a method to compute the asymptotic bounds in the form of condition numbers for constrained reachability probabilities against perturbations of the distribution parameters of the system. The adequacy of the method is demonstrated through experiments with the Zeroconf protocol and the hopping frog problem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
