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.