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.