Premium
Formal verification of tail distribution bounds in the HOL theorem prover
Author(s) -
Hasan Osman,
Tahar Sofiène
Publication year - 2008
Publication title -
mathematical methods in the applied sciences
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.719
H-Index - 65
eISSN - 1099-1476
pISSN - 0170-4214
DOI - 10.1002/mma.1055
Subject(s) - mathematics , markov chain , random variable , automated theorem proving , chebyshev filter , discrete mathematics , bernoulli distribution , algorithm , statistics , mathematical analysis
Tail distribution bounds play a major role in the estimation of failure probabilities in performance and reliability analysis of systems. They are usually estimated using Markov's and Chebyshev's inequalities, which represent tail distribution bounds for a random variable in terms of its mean or variance. This paper presents the formal verification of Markov's and Chebyshev's inequalities for discrete random variables using a higher‐order‐logic theorem prover. The paper also provides the formal verification of mean and variance relations for some of the widely used discrete random variables, such as Uniform( m ), Bernoulli( p ), Geometric( p ) and Binomial( m, p ) random variables. This infrastructure allows us to precisely reason about the tail distribution properties and thus turns out to be quite useful for the analysis of systems used in safety‐critical domains, such as space, medicine or transportation. For illustration purposes, we present the performance analysis of the coupon collector's problem, a well‐known commercially used algorithm. Copyright © 2008 John Wiley & Sons, Ltd.