Verification of Tail Distribution Bounds in a Theorem Prover

摘要

In the field of probabilistic analysis, bounding the tail distribution is a major tool for estimating the failure probability of systems. In this paper, we present the verification of Markov's and Chebyshev's inequalities for discrete random variables using the HOL theorem prover. The formally verified Markov and Chebyshev's inequalities allow us to precisely reason about tail distribution bounds for probabilistic systems within the core of a higher-order-logic theorem prover and thus prove to be quite useful for the analysis of systems used in safety-critical domains, such as space, medicine and military. For illustration purposes, we show how we can obtain bounds on the tail distribution of the Coupon Collector's problem in HOL.