KMS Of Academy of mathematics and systems sciences, CAS
Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters | |
Su, Guoxin1; Feng, Yuan2,3; Chen, Taolue4; Rosenblum, David S.1 | |
2016-07-01 | |
发表期刊 | IEEE TRANSACTIONS ON SOFTWARE ENGINEERING |
ISSN | 0098-5589 |
卷号 | 42期号:7页码:623-639 |
摘要 | Probabilistic model checking is a verification technique that has been the focus of intensive research for over a decade. One important issue with probabilistic model checking, which is crucial for its practical significance but is overlooked by the state-of-the-art largely, is the potential discrepancy between a stochastic model and the real-world system it represents when the model is built from statistical data. In the worst case, a tiny but nontrivial change to some model quantities might lead to misleading or even invalid verification results. To address this issue, in this paper, we present a mathematical characterization of the consequences of model perturbations on the verification distance. The formal model that we adopt is a parametric variant of discrete-time Markov chains equipped with a vector norm to measure the perturbation. Our main technical contributions include a closed-form formulation of asymptotic perturbation bounds, and computational methods for two arguably most useful forms of those bounds, namely linear bounds and quadratic bounds. We focus on verification of reachability properties but also address automata-based verification of omega-regular properties. We present the results of a selection of case studies that demonstrate that asymptotic perturbation bounds can accurately estimate maximum variations of verification results induced by model perturbations. |
关键词 | Asymptotic perturbation bound discrete-time Markov chain numerical iteration optimization parametric Markov chain perturbation analysis probabilistic model checking quadratic programming |
DOI | 10.1109/TSE.2015.2508444 |
语种 | 英语 |
资助项目 | Singapore Ministry of Education[R-252-000-458-133] ; Australian Research Council[DP130102764] ; Australian Research Council[DP160101652] ; National Natural Science Foundation of China[61428208] ; National Natural Science Foundation of China[61502260] ; CAS/SAFEA International Partnership Program for Creative Research Team ; State Key Laboratory of Novel Software Technology at Nanjing University |
WOS研究方向 | Computer Science ; Engineering |
WOS类目 | Computer Science, Software Engineering ; Engineering, Electrical & Electronic |
WOS记录号 | WOS:000380053500002 |
出版者 | IEEE COMPUTER SOC |
引用统计 | |
文献类型 | 期刊论文 |
条目标识符 | http://ir.amss.ac.cn/handle/2S8OKBNM/23254 |
专题 | 中国科学院数学与系统科学研究院 |
通讯作者 | Su, Guoxin |
作者单位 | 1.Natl Univ Singapore, Sch Comp, Dept Comp Sci, Singapore 117548, Singapore 2.Univ Technol Sydney, Ctr Quantum Computat & Intelligent Syst, Sydney, NSW 2007, Australia 3.Chinese Acad Sci, AMSS UTS Joint Res Lab Quantum Computat, Beijing 100864, Peoples R China 4.Middlesex Univ, Dept Comp Sci, London, England |
推荐引用方式 GB/T 7714 | Su, Guoxin,Feng, Yuan,Chen, Taolue,et al. Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,2016,42(7):623-639. |
APA | Su, Guoxin,Feng, Yuan,Chen, Taolue,&Rosenblum, David S..(2016).Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters.IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,42(7),623-639. |
MLA | Su, Guoxin,et al."Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters".IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 42.7(2016):623-639. |
条目包含的文件 | 条目无相关文件。 |
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。
修改评论