Abstract
Expectation (average) properties of continuous random variables are widely used to judge performance characteristics in engineering and physical sciences. This paper presents an infrastructure that can be used to formally reason about expectation properties of most of the continuous random variables in a theorem prover. Starting from the relatively complex higher-order-logic definition of expectation, based on Lebesgue integration, we formally verify key expectation properties that allow us to reason about expectation of a continuous random variable in terms of simple arithmetic operations. In order to illustrate the practical effectiveness and utilization of our approach, we also present the formal verification of expectation properties of the commonly used continuous random variables: Uniform, Triangular and Exponential.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Akbarpour, B., Tahar, S.: An Approach for the Formal Verification of DSP Designs using Theorem Proving. IEEE Transactions on CAD of Integrated Circuits and Systems 25(8), 1141–1457 (2006)
Audebaud, P., Paulin-Mohring, C.: Proofs of Randomized Algorithms in Coq. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 49–68. Springer, Heidelberg (2006)
Bialas, J.: The σ-Additive Measure Theory. J. of Formalized Mathematics 2 (1990)
Coble, A.: On Probability, Measure, and Integration in HOL4. Technical Report, Computing Laboratory, University of Cambridge, UK (2009), http://www.srcf.ucam.org/~arc54/techreport.pdf
Daumas, M., Martin-Dorel, E., Lester, D., Truffert, A.: Stochastic Formal Correctness of Numerical Allgorithms. In: First NASA Formal Methods Symposium, pp. 136–145 (2009)
Devroye, L.: Non-Uniform Random Variate Generation. Springer, Heidelberg (1986)
Galambos, J.: Advanced Probability Theory. Marcel Dekker Inc., New York (1995)
Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)
Harrison, J.: Floating Point Verification in HOL Light: The Exponential Function. Technical Report 428, Computing Laboratory, University of Cambridge, UK (1997)
Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998)
Hasan, O.: Formal Probabilistic Analysis using Theorem Proving. PhD Thesis, Concordia University, Montreal, QC, Canada (2008)
Hasan, O., Abbasi, N., Tahar, S.: Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 277–291. Springer, Heidelberg (2009)
Hasan, O., Tahar, S.: Performance Analysis of ARQ Protocols using a Theorem Prover. In: Proc. International Symposium on Performance Analysis of Systems and Software, pp. 85–94. IEEE Computer Society, Los Alamitos (2008)
Hasan, O., Tahar, S.: Performance Analysis of Wireless Systems using Theorem Proving. In: Proc. First International Workshop on Formal Methods for Wireless Systems, Toronto, ON, Canada, pp. 3–18 (2008)
Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD Thesis, University of Cambridge, Cambridge, UK (2002)
Mitzenmacher, M., Upfal, E.: Probability and Computing. Cambridge University Press, Cambridge (2005)
Nedzusiak, A.: σ-fields and Probability. J. of Formalized Mathematics 1 (1989)
Richter, S.: Formalizing Integration Theory, with an Application to Probabilistic Algorithms. Diploma Thesis, Technische Universität München, Department of Informatics, Germany (2003)
Widrow, B.: Statistical Analysis of Amplitude-quantized Sampled Data Systems. AIEE Trans. (Applications and Industry) 81, 555–568 (1961)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hasan, O., Abbasi, N., Akbarpour, B., Tahar, S., Akbarpour, R. (2009). Formal Reasoning about Expectation Properties for Continuous Random Variables. In: Cavalcanti, A., Dams, D.R. (eds) FM 2009: Formal Methods. FM 2009. Lecture Notes in Computer Science, vol 5850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-05089-3_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-05089-3_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-05088-6
Online ISBN: 978-3-642-05089-3
eBook Packages: Computer ScienceComputer Science (R0)