Mhamdi, Tarek, Hasan, Osman and Tahar, Sofiène (2013) Formalization of Measure Theory and Lebesgue Integration for Probabilistic Analysis in HOL. ACM Transactions on Embedded Computing Systems, 12 (1). pp. 123. ISSN 15399087

Text (application/pdf)
410kBTECS2013.pdf  Accepted Version 
Official URL: http://dx.doi.org/10.1145/2406336.2406349
Abstract
Dynamic systems that exhibit probabilistic behavior represent a large class of manmade systems such as communication networks, air traffic control, and other missioncritical systems. Evaluation of quantitative issues like performance and dependability of these systems is of paramount importance. In this paper, we propose a generalized methodology to formally reason about probabilistic systems within a theorem prover. We present a formalization of measure theory in the HOL theorem prover and use it to formalize basic concepts from the theory of probability. We also use the Lebesgue integration to formalize statistical properties of random variables. To illustrate the practical effectiveness of our methodology, we formally prove classical results from the theories of probability and information and use them in a data compression application in HOL.
Divisions:  Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering 

Item Type:  Article 
Refereed:  Yes 
Authors:  Mhamdi, Tarek and Hasan, Osman and Tahar, Sofiène 
Journal or Publication:  ACM Transactions on Embedded Computing Systems 
Date:  January 2013 
Digital Object Identifier (DOI):  10.1145/2406336.2406349 
Keywords:  information theory; lebesgue integration; measure theory; probabilistic systems; proof theory; reliability; statistical properties; theorem proving; verification; 
ID Code:  977357 
Deposited By:  DANIELLE DENNIE 
Deposited On:  14 Jun 2013 13:06 
Last Modified:  18 Jan 2018 17:44 
References:
1Christel Baier , JoostPieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Press, 20082Christel Baier , Boudewijn Haverkort , Holger Hermanns , JoostPieter Katoen, ModelChecking Algorithms for ContinuousTime Markov Chains, IEEE Transactions on Software Engineering, v.29 n.6, p.524541, June 2003 [doi>10.1109/TSE.2003.1205180]
3Berberian, S. K. 1998. Fundamentals of Real Analysis. Springer.
4Bialas, J. 1990. The σadditive measure theory. J. Formal. Math. 2.
5Bogachev, V. I. 2006. Measure Theory. Springer.
6D. Chaum, The dining cryptographers problem: unconditional sender and recipient untraceability, Journal of Cryptology, v.1 n.1, p.6575, 1988
7Coble, A. R. 2010. Anonymity, information, and machineassisted proof. Ph.D. thesis, University of Cambridge.
8Thomas M. Cover , Joy A. Thomas, Elements of information theory, WileyInterscience, New York, NY, 1991
9de Alfaro, L. 1997. Ph.D. thesis, Stanford University.
10Fraenkel, A., BarHillel, Y., and Levy, A. 1973. Foundations of Set Theory. North Holland.
11Michael J. C. Gordon, Mechanizing programming logics in higher order logic, Current trends in hardware verification and automated theorem proving, SpringerVerlag New York, Inc., New York, NY, 1989
12M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993
13Halmos, P. R. 1944. The foundations of probability. Amer. Math. Monthly 51, 9, 493510.
14John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, New York, NY, 2009
15Osman Hasan , Sofiène Tahar, Verification of expectation properties for discrete random variables in HOL, Proceedings of the 20th international conference on Theorem proving in higher order logics, p.119134, September 1013, 2007, Kaiserslautern, Germany
16Hasan, O. and Tahar, S. 2009a. Formal verification of tail distribution bounds in the HOL theorem prover. Math. Methods Appl. Sci. 32, 4 (March), 480504.
17Osman Hasan , Sofiène Tahar, Performance Analysis and Functional Verification of the StopandWait Protocol in HOL, Journal of Automated Reasoning, v.42 n.1, p.133, January 2009 [doi>10.1007/s1081700891056]
18Osman Hasan , Naeem Abbasi , Behzad Akbarpour , Sofiène Tahar , Reza Akbarpour, Formal Reasoning about Expectation Properties for Continuous Random Variables, Proceedings of the 2nd World Congress on Formal Methods, November 0206, 2009, Eindhoven, The Netherlands [doi>10.1007/9783642050893_28]
19Osman Hasan , Sofiene Tahar , Naeem Abbasi, Formal Reliability Analysis Using Theorem Proving, IEEE Transactions on Computers, v.59 n.5, p.579592, May 2010 [doi>10.1109/TC.2009.165]
20Hurd, J. 2002. Formal verifcation of probabilistic algorithms. Ph.D. thesis, University of Cambridge.
21Marta Kwiatkowska , Gethin Norman , David Parker, Quantitative Analysis With the Probabilistic Model Checker PRISM, Electronic Notes in Theoretical Computer Science (ENTCS), v.153 n.2, p.531, May, 2006 [doi>10.1016/j.entcs.2005.10.030]
22David R Lester, Topology in PVS: continuous mathematics with applications, Proceedings of the second workshop on Automated formal methods, p.1120, November 0606, 2007, Atlanta, Georgia [doi>10.1145/1345169.1345171]
23Mhamdi, T., Hasan, O., and Tahar, S. 2010a. Formal analysis of systems with probabilistic behavior in HOL. http://users.encs.concordia.ca/~mhamdi/hol/probability/.
24Tarek Mhamdi , Osman Hasan , Sofiène Tahar, On the formalization of the lebesgue integration theory in HOL, Proceedings of the First international conference on Interactive Theorem Proving, July 1114, 2010, Edinburgh, UK [doi>10.1007/9783642140525_27]
25Nȩdzusiak, A. 1989. σfields and Probability. J. Formal. Math. 1.
26Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748752, June 1518, 1992
27Papoulis, A. 1984. Probability, Random Variables, and Stochastic Processes. McGraw Hill.
28Parker, D. 2001. Ph.D. thesis, University of Birmingham, Birmingham, UK.
29Paulson, L. C. 1994. Isabelle: A Generic Theorem Prover. Springer.
30Michael K. Reiter , Aviel D. Rubin, Crowds: anonymity for Web transactions, ACM Transactions on Information and System Security (TISSEC), v.1 n.1, p.6692, Nov. 1998 [doi>10.1145/290163.290168]
31Richter, S. 2004. Formalizing integration theory with an application to probabilistic algorithms. In Proceedings of the 17the International Conference on Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science. vol. 3223. 271286.
32Rutten, J., Kwaiatkowska, M., Normal, G., and Parker, D. 2004. Mathematical Techniques for Analyzing Concurrent and Probabilisitc Systems. CRM Monograph Series, vol. 23. American Mathematical Society.
33Koushik Sen , Mahesh Viswanathan , Gul Agha, VESTA: A Statistical Modelchecker and Analyzer for Probabilistic Systems, Proceedings of the Second International Conference on the Quantitative Evaluation of Systems, p.251, September 1922, 2005 [doi>10.1109/QEST.2005.42]
34Geoffrey Smith, On the Foundations of Quantitative Information Flow, Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, March 2229, 2009, York, UK [doi>10.1007/9783642005961_21]
35Wagon, S. 1993. The BanachTarski Paradox. Cambridge University Press.
Repository Staff Only: item control page