Abstract

Probabilistic analysis is a tool of fundamental importance to virtually all scientists and engineers as they often have to deal with systems that exhibit random or unpredictable elements. Traditionally, computer simulation techniques are used to perform probabilistic analysis. However, they provide less accurate results and cannot handle large-scale problems due to their enormous computer processing time requirements. To overcome these limitations, this thesis proposes to perform probabilistic analysis by formally specifying the behavior of random systems in higher-order logic and use these models for verifying the intended probabilistic and statistical properties in a computer based theorem prover. The analysis carried out in this way is free from any approximation or precision issues due to the mathematical nature of the models and the inherent soundness of the theorem proving approach. The thesis mainly targets the two most essential components for this task, i.e., the higher-order-logic formalization of random variables and the ability to formally verify the probabilistic and statistical properties of these random variables within a theorem prover. We present a framework that can be used to formalize and verify any continuous random variable for which the inverse of the cumulative distribution function can be expressed in a closed mathematical form. Similarly, we provide a formalization infrastructure that allows us to formally reason about statistical properties, such as mean, variance and tail distribution bounds, for discrete random variables. In order to in illustrate the practical effectiveness of the proposed approach, we consider the probabilistic analysis of three examples: the Coupon Collector's problem, the roundoff error in a digital processor and the Stop-and-Wait protocol. All the above mentioned work is conducted using the HOL theorem prover.