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. 1-23. ISSN 15399087
Preview |
Text (application/pdf)
410kBTECS-2013.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 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. 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 , Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Press, 20082Christel Baier , Boudewijn Haverkort , Holger Hermanns , Joost-Pieter Katoen, Model-Checking Algorithms for Continuous-Time Markov Chains, IEEE Transactions on Software Engineering, v.29 n.6, p.524-541, 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.65-75, 1988
7Coble, A. R. 2010. Anonymity, information, and machine-assisted proof. Ph.D. thesis, University of Cambridge.
8Thomas M. Cover , Joy A. Thomas, Elements of information theory, Wiley-Interscience, New York, NY, 1991
9de Alfaro, L. 1997. Ph.D. thesis, Stanford University.
10Fraenkel, A., Bar-Hillel, 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, Springer-Verlag 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, 493--510.
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.119-134, September 10-13, 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), 480--504.
17Osman Hasan , Sofiène Tahar, Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL, Journal of Automated Reasoning, v.42 n.1, p.1-33, January 2009 [doi>10.1007/s10817-008-9105-6]
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 02-06, 2009, Eindhoven, The Netherlands [doi>10.1007/978-3-642-05089-3_28]
19Osman Hasan , Sofiene Tahar , Naeem Abbasi, Formal Reliability Analysis Using Theorem Proving, IEEE Transactions on Computers, v.59 n.5, p.579-592, 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.5-31, 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.11-20, November 06-06, 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 11-14, 2010, Edinburgh, UK [doi>10.1007/978-3-642-14052-5_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.748-752, June 15-18, 1992
27Papoulis, A. 1984. Probability, Random Variables, and Stochastic Processes. Mc-Graw 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.66-92, 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. 271--286.
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 Model-checker and Analyzer for Probabilistic Systems, Proceedings of the Second International Conference on the Quantitative Evaluation of Systems, p.251, September 19-22, 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 22-29, 2009, York, UK [doi>10.1007/978-3-642-00596-1_21]
35Wagon, S. 1993. The Banach-Tarski Paradox. Cambridge University Press.
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.
Repository Staff Only: item control page
Download Statistics
Download Statistics