Verification of Probabilistic Models in Interactive Theorem Provers

许多自然和技术系统都具有随机性。在信息学中，随机性经常被用来提高稳健性或效率。模型检测是一种自动分析(验证)具有有限状态空间的系统的方法。在过去的15年里，概率系统的模型检测已经成为一个非常活跃的研究领域。信息学中第二个重要的验证技术是借助定理证明器的交互验证。在过去的十年里，这一领域取得了快速的进展。例如，验证真实的编译器和操作系统内核已经成为可能。与此同时，概率论在定理证明者中的形式化开始了。作为应用，概率模型检验最近首次在交互式定理证明器中得到验证。这一建议的目的是在定理证明器中形式化概率系统的数学基础，以便验证不能自动验证的复杂算法和系统。作为具体的应用，我们将对分布式计算机系统中的一些参数概率算法进行交互验证，形式化(自动或交互)验证的动机是其极高的可靠性。这与概率系统的证明尤其相关：例如，由于随机变量之间的微妙相关性，概率系统比确定性系统更容易出错。互动式核查始于并充分利用了数学基础，这大大增加了它的可靠性，特别是它的灵活性。这就是为什么参数系统是交互验证中的规范和固定参数是例外的原因。由于这种灵活性和开放性，信息学的重要基础在定理谚语中的形式化已经成为一个全球性的项目。到目前为止，编程语言和编译器已经被特别广泛地讨论过。我们建议的目的是在定理证明器中完全形式化概率模型(以及其相应的模型检验过程)：以便能够应用如参数系统的验证，但也通过这一重要领域扩展信息学数学基础的形式化。我们认为这是对计算机系统可靠性的长期投资。

Many natural and technical systems are of a stochastic nature. Ininformatics, randomness is often employed to increase robustness orefficiency. Model checking is a method for automatically analysing(`verifying') systems with a finite state space. In the past 15 years, modelchecking for probabilistic systems has become a very active research area.The second important verification technique in informatics is interactiveverification with the help of a theorem prover. This area has made rapidprogress over the past decade. For example, it has become possible toverify realistic compilers and operating system kernels. At the same time,the formalisation of probability theory in theorem provers started. Asan application, probabilistic model checking was recently verified in aninteractive theorem prover for the first time. The aim of this grantproposal is the formalisation of the mathematical basis of probabilisticsystems in a theorem prover in order to verify complicated algorithms andsystems that cannot be verified automatically. As concrete applications wewill verify interactively a number of parametric probabilistic algorithmsfor distributed computer systems.The motivation for formal (automatic or interactive) verification is itsextremely high reliability. This is particularly relevant for proofs ofprobabilistic systems: they are much more error prone than fordeterministic systems, for example, because of subtle dependencies betweenrandom variables. Interactive verification starts with and has full accessto the mathematical foundations, which increases its reliability and inparticular its flexibility enormously. This is the reason why parametricsystems are the norm and fixed parameters the exception in interactiveverification. Because of this flexibility and open-endedness, theformalisation of important foundations of informatics in theorem provershas become a global project. So far, programming languages and compilershave been covered particularly extensively. The aim of our proposal is acomplete formalisation of probabilistic models (and, as case studies, theircorresponding model checking procedures) in a theorem prover: In order toenable applications like the verification of parametric systems, but alsoto extend the formalisation of the mathematical foundations of informaticsby this important area. We view this as a long-term investment into thereliability of computer systems.