Technical Report
Formalization
of Continuous Probability Distributions
O.
Hasan and S. Tahar
ABSTRACT
In order to overcome the limitations of state-of-the-art simulation based probabilistic analysis, we propose to perform probabilistic analysis within the environment of a higher-order-logic theorem prover. The foremost requirement for conducting such analysis is the formalization of probability distributions. In this report, we present a methodology for the formalization of continuous probability distributions for which the inverse of the cumulative distribution function can be expressed in a closed mathematical form. Our methodology is primarily based on the formalization of the Standard Uniform random variable, cumulative distribution function properties and the Inverse Transform method. The report presents all this formalization using the HOL theorem prover. In order to illustrate the practical effectiveness of our methodology, the formalization of a few continuous probability distributions has also been included.
|
|
|
|
|
|
|
|
Download
PDF file (