Verification of Probabilistic Models in Interactive Theorem Provers

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

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.