Abstract
Traditionally, simulation is used to perform probabilistic analysis. However, it provides less accurate results and cannot handle large-scale problems due to the enormous CPU time requirements. Recently, a significant amount of formalization has been done in higher-order logic that allows us to conduct precise probabilistic analysis using theorem proving and thus overcome the limitations of the simulation. Some major contributions include the formalization of both discrete and continuous random variables and the verification of some of their corresponding probabilistic and statistical properties. This paper describes the infrastructures behind these capabilities and their utilization to conduct the probabilistic analysis of real-world systems.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
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)
Andrews, Z.: Towards a Stochastic Event B for Designing Dependable Systems. In: Proc. Workshop on Quantitative Formal Methods: Theory and Applications, Eindhoven, The Netherlands (November 2009)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model Checking Algorithms for Continuous time Markov Chains. IEEE Transactions on Software Engineering 29(4), 524–541 (2003)
Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)
Cardell-Oliver, R.: The Formal Verification of Hard Real-time Systems. PhD Thesis, University of Cambridge, UK (1992)
Coble, A.: Anonymity, Information, and Machine-Assisted Proof. Ph.D Thesis, University of Cambridge, UK (2009)
Corin, R.J., Den Hartog, J.I.: A Probabilistic Hoare-style Logic for Game-based Cryptographic Proofs. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 252–263. Springer, Heidelberg (2006)
de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD Thesis, Stanford University, Stanford, USA (1997)
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.: Mechanizing Programming Logics in Higher-Order Logic. In: Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387–439. Springer, Heidelberg (1989)
Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)
Hallerstede, S., Hoang, T.S.: Qualitative Probabilistic Modelling in Event-B. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 293–312. Springer, Heidelberg (2007)
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)
Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009)
Hasan, O., Abbasi, N., Akbarpour, B., Tahar, S., Akbarpour, R.: Formal reasoning about expectation properties for continuous random variables. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009: Formal Methods. LNCS, vol. 5850, pp. 435–450. Springer, Heidelberg (2009)
Hasan, O., Tahar, S.: Formalization of the Continuous Probability Distributions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 3–18. Springer, Heidelberg (2007)
Hasan, O., Tahar, S.: Formalization of the Standard Uniform Random Variable. Theoretical Computer Science 382(1), 71–83 (2007)
Hasan, O., Tahar, S.: Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. Journal of Automated Reasoning 41(3-4), 295–323 (2008)
Hasan, O., Tahar, S.: Formal Verification of Tail Distribution Bounds in the HOL Theorem Prover. Mathematical Methods in the Applied Sciences 32(4), 480–504 (2009)
Hasan, O., Tahar, S.: Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL. Journal of Automated Reasoning 42(1), 1–33 (2009)
Hasan, O., Tahar, S., Abbasi, N.: Formal Reliability Analysis using Theorem Proving. IEEE Transactions on Computers (2009), doi:10.1109/TC.2009.165
Hermanns, H., Katoen, J.P., Meyer-Kayser, J., Siegle, M.: A Markov Chain Model Checker. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 347–362. Springer, Heidelberg (2000)
Hoang, T.S.: The Development of a Probabilistic B Method and a Supporting Toolkit. PhD Thesis, The University of New South Wales, UK (2005)
Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD Thesis, University of Cambridge, UK (2002)
Jeannet, B., Argenio, P.D., Larsen, K.: Rapture: A Tool for Verifying Markov Decision Processes. In: Tools Day, 13th Int. Conf. Concurrency Theory, Brno, Czech Republic (2002)
Kwiatkowska, M., Norman, G., Parker, D.: Quantitative Analysis with the Probabilistic Model Checker PRISM. Electronic Notes in Theoretical Computer Science 153(2), 5–31 (2005)
Leon-Garcia, A., Widjaja, I.: Communication Networks: Fundamental Concepts and Key Architectures. McGraw-Hill, New York (2004)
Levine, A.: Theory of Probability. Addison-Wesley series in Behavioral Science, Quantitative Methods (1971)
MacKay, D.J.C.: Introduction to Monte Carlo Methods. In: Learning in Graphical Models, NATO Science Series, pp. 175–204. Kluwer Academic Press, Dordrecht (1998)
McIver, A., Meinicke, L., Morgan, C.: Security, Probability and Nearly Fair Coins in the Cryptographers’ Café. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009: Formal Methods. LNCS, vol. 5850, pp. 41–71. Springer, Heidelberg (2009)
Miczo, A.: Digital Logic Testing and Simulation. Wiley Interscience, Hoboken (2003)
Mitzenmacher, M., Upfal, E.: Probability and Computing. Cambridge University Press, Cambridge (2005)
Parker, D.: Implementation of Symbolic Model Checking for Probabilistic System. PhD Thesis, University of Birmingham, UK (2001)
PRISM (2008), http://www.cs.bham.ac.uk/~dxp/prism
Rutten, J., Kwaiatkowska, M., Normal, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilisitc Systems. CRM Monograph Series, vol. 23. American Mathematical Society (2004)
Sen, K., Viswanathan, M., Agha, G.: VESTA: A Statistical Model-Checker and Analyzer for Probabilistic Systems. In: Proc. IEEE International Conference on the Quantitative Evaluation of Systems, pp. 251–252 (2005)
Shi, W., Fuchs, W.K.: Probabilistic Analysis and Algorithms for Reconfiguration of Memory Arrays. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 11(9), 1153–1160 (1992)
White, N.: Probabilistic Specification and Refinement. Masters Thesis, Oxford University, UK (1996)
Widrow, B.: Statistical Analysis of Amplitude-quantized Sampled Data Systems. AIEE Transactions on Applications and Industry 81, 555–568 (1961)
Yates, R.D., Goodman, D.J.: Probability and Stochastic Processes: A Friendly Introduction for Electrical and Computer Engineers. Wiley, Chichester (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hasan, O., Tahar, S. (2010). Formal Probabilistic Analysis: A Higher-Order Logic Based Approach. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds) Abstract State Machines, Alloy, B and Z. ABZ 2010. Lecture Notes in Computer Science, vol 5977. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11811-1_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-11811-1_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11810-4
Online ISBN: 978-3-642-11811-1
eBook Packages: Computer ScienceComputer Science (R0)