Perturbation Analysis for Probabilistic Verification

这个项目主要关注概率模型检查（PMC），它增强了经典模型检查技术来验证随机系统的各种定量特性，例如可靠性、安全性和性能。PMC已经见证了随机算法、网络协议设计、机器人和系统生物学等领域的成功应用。目前概率模型检验的实践通常假设随机模型中的数值量（例如，转移概率，转移率）是精确已知的，或者可以精确获得。这是一个方便的假设，但不幸的是过于简化了。事实上，现实世界的系统，例如来自工程、生物学或经济学的系统，都是由参数控制的，这些参数的值必须经过经验估计。这些值具有统计性质，因此会受到扰动，这就提出了验证结果的敏感性或鲁棒性问题。研究表明，即使是很小的概率扰动也可能导致验证结果发生显著变化，因此使用现有PMC算法和工具获得的结果可能具有误导性甚至无效。为了解决这个问题，我们建议进行摄动分析，即分析验证结果如何受到参数摄动的影响，并提供量化的度量。具体地说，我们将首先研究如何正式地定义度量，可能是在各种形式的扰动界中。然后，我们将开发高效的算法来计算这些摄动界，并确定它们的计算复杂度。最后，我们将开发软件工具来促进微扰分析。该工具包将用于对现实世界问题进行案例研究，以全面评估我们的方法并展示其适用性和重要性。

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.