Formalization of the Heavy Hitter Problem in HOL

Technical Report

Abstract
Dynamic and real systems that exhibit probabilistic behavior represent a large class of man- made systems such as communication networks, air traffic control and other mission critical systems. Evaluation of quantitative issues like performance and dependability of these systems is of paramount importance. Probabilistic analysis is an indispensable tool for all scientists and engineers since they are often dealing with systems containing elements that exhibit random or unpredictable behavior. Traditionally, computer simulation techniques have been used to perform probabilistic analysis. However, they provide less accurate results and cannot handle large problems due to enormous computer processing time requirements. We have developed a generalized framework for the probabilistic analysis of systems using the HOL theorem prover. We present the formalization of extended reals in Higher-Order logic. This formalization is used to formalize other theories such as Measure and Probability theories. We then used our formalization of extended real numbers and the already existing formalization of Measure, Lebesgue Integration and Probability theories to model an algorithm for the Heavy Hitter problem. This model is then utilized to formally verify some interesting probabilistic and statistical properties associated with the heavy hitter problem in HOL.

Files

• Technical Report: PDF File
• Appendix: HOL signature