Perturbation Analysis for Probabilistic Verification

点击翻译按钮获取中文摘要

This project mainly concerns probabilistic model checking (PMC), which enhances classical model checking techniques to verify stochastic systems against various quantitative properties, for instance, reliability, security, and performance. PMC has witnessed successful applications from domains as diverse as randomised algorithms, network protocol design, robotics, and systems biology. Current practice of probabilistic model checking usually assumes that numerical quantities (e.g., transition probabilities, transition rates) in stochastic models are known exactly, or can be acquired precisely. This is a handy, but unfortunately oversimplified, assumption. Indeed, real-world systems, for instance those from engineering, biology, or economics, are governed by parameters whose values must be empirically estimated. These values are of a statistical nature and thus are subject to perturbations, which raises the sensitivity or robustness issue of the verification results. Research has demonstrated that even small perturbations of probabilities might lead to significant variations in the verification result, and thus the results obtained using existing PMC algorithms and tools can be misleading or even invalid. To tackle this issue, we propose to carry out perturbation analysis, i.e., to analyse how the verification result is affected by the perturbation of parameters and to provide a quantitative measure thereof. Concretely speaking, we will first investigate how to define the measures formally, possibly in various forms of perturbation bounds. Then we will develop efficient and effective algorithms to compute these perturbation bounds, and identify their computational complexity. Finally, we will develop software tools to facilitate the perturbation analysis. The toolkit will be employed to conduct case studies on real-world problems for a thorough evaluation of our approach and demonstration of its applicability and significance.