Perturbation Analysis in Verification of Discrete-Time Markov Chains
Perturbation Analysis in Verification of Discrete-Time Markov Chains
复制标题
离散时间马尔可夫链验证中的扰动分析
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Guoxin Su
中科院分区：
文献类型：
--
作者：
Taolue Chen;Yuan Feng;David S. Rosenblum;Guoxin Su
概率验证中的扰动分析解决了随机模型对定性和定量属性验证的鲁棒性和敏感性问题。我们确定两种类型的扰动界，即非渐近界和渐近界。非渐近边界是精确的逐点边界，其量化了受模型的给定扰动影响的验证结果的上界和下界，而渐近边界是通过假设给定扰动足够小来近似非渐近边界的封闭形式边界。我们在离散时间马尔可夫链的背景下进行扰动分析。我们考虑三个基本的矩阵范数捕获的扰动距离，并专注于计算方面。我们的主要贡献包括算法和严格的复杂性界计算非渐近界和渐近界相对于三个扰动距离。
Perturbation analysis in probabilistic verification addresses the robustness and sensitivity problem for verification of stochastic models against qualitative and quantitative properties. We identify two types of perturbation bounds, namely non-asymptotic bounds and asymptotic bounds. Non-asymptotic bounds are exact, pointwise bounds that quantify the upper and lower bounds of the verification result subject to a given perturbation of the model, whereas asymptotic bounds are closed-form bounds that approximate non-asymptotic bounds by assuming that the given perturbation is sufficiently small. We perform perturbation analysis in the setting of Discrete-time Markov Chains. We consider three basic matrix norms to capture the perturbation distance, and focus on the computational aspect. Our main contributions include algorithms and tight complexity bounds for calculating both non-asymptotic bounds and asymptotic bounds with respect to the three perturbation distances.