Skip to main content
SpringerLink
Log in

Formalization of Continuous Probability Distributions

  • Conference paper
Automated Deduction – CADE-21 (CADE 2007)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 4603))

Included in the following conference series:

Abstract

Continuous probability distributions are widely used to mathematically describe random phenomena in engineering and physical sciences. In this paper, we present a methodology that can be used to formalize any continuous random variable for which the inverse of the cumulative distribution function can be expressed in a closed mathematical form. Our methodology is primarily based on the Standard Uniform random variable, the classical cumulative distribution function properties and the Inverse Transform method. The paper includes the higher-order-logic formalization details of these three components in the HOL theorem prover. To illustrate the practical effectiveness of the proposed methodology, we present the formalization of Exponential, Uniform, Rayleigh and Triangular random variables.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Akbarpour, B., Tahar, S.: Formalization of Fixed-Point Arithmetic in HOL. Formal Methods in Systems Design 27(1-2), 173–200 (2005)

    Article  MATH  Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P: Model Checking Algorithms for Continuous time Markov Chains. IEEE Trans. on Software Engineering 29(4), 524–541 (2003)

    Article  Google Scholar 

  4. Clarke, E.M, Grumberg, O., Peled, D.A: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  5. Devroye, L.: Non-Uniform Random Variate Generation. Springer, Heidelberg (1986)

    MATH  Google Scholar 

  6. Gonsalves, T.A, Tobagi, F.A: On the Performance Effects of Station Locations and Access Protocol Parameters in Ethernet Networks. IEEE Trans. on Communications 36(4), 441–449 (1988)

    Article  Google Scholar 

  7. Gordon, M.J.C: Mechanizing Programming Logics in Higher-0rder Logic. In: Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387–439. Springer, Heidelberg (1989)

    Google Scholar 

  8. Gordon, M.J.C, Melham, T.F: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  9. Gupta, V.T, Jagadeesan, R., Panangaden, P.: Stochastic Processes as Concurrent Constraint Programs. In: Principles of Programming Languages, pp. 189–202. ACM Press, New York (1999)

    Google Scholar 

  10. Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  11. Hasan, O., Tahar, S.: Formalization of the Standard Uniform Random Variable. Theoretical Computer Science (to appear)

    Google Scholar 

  12. Hasan, O., Tahar, S.: Verification of Probabilistic Properties in HOL using the Cumulative Distribution Function. In: Integrated Formal Methods. LNCS, vol. 4591, pp. 333–352. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  13. Hasan, O., Tahar, S.: Formalization of Continuous Probability Distributions. Technical Report, Concordia University, Montreal, Canada (February 2007), http://hvg.ece.concordia.ca/Publications/TECH_REP/FCPD_TR07

  14. Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD Thesis, University of Cambridge, Cambridge, UK (2002)

    Google Scholar 

  15. Kaneko, T., Liu, B.: On Local Roundoff Errors in Floating-Point Arithmetic. ACM 20(3), 391–398 (1973)

    Article  MATH  MathSciNet  Google Scholar 

  16. Khazanie, R.: Basic Probability Theory and Applications. Goodyear (1976)

    Google Scholar 

  17. Köpsel, A., Ebert, J., Wolisz, A.: A Performance Comparison of Point and Distributed Coordination Function of an IEEE 802.11 WLAN in the Presence of Real-Time Requirements. In: Proceedings of Seventh International Workshop on Mobile Multimedia Communications, Tokyo, Japan (2000)

    Google Scholar 

  18. Mitzenmacher, M., Upfal, E.: Probability and Computing. Cambridge University Press, Cambridge (2005)

    MATH  Google Scholar 

  19. Park, S., Pfenning, F., Thrun, S.: A Probabilistic Language based upon Sampling Functions. In: Principles of Programming Languages, pp. 171–182. ACM Press, New York (2005)

    Google Scholar 

  20. Pfeffer, A.: IBAL: A Probabilistic Rational Programming Language. In: International Joint Conferences on Artificial Intelligence, pp. 733–740. Morgan Kaufmann Publishers, Washington (2001)

    Google Scholar 

  21. Ross, S.M: Simulation. Academic Press, San Diego (2002)

    Google Scholar 

  22. Rutten, J., Kwaiatkowska, M., Normal, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilisitc Systems. CRM Monograph Series. American Mathematical Society, vol. 23 (2004)

    Google Scholar 

  23. Tridevi, K.S: Probability and Statistics with Reliability, Queuing and Computer Science Applications. Wiley, Chichester (2002)

    Google Scholar 

  24. Widrow, B.: Statistical Analysis of Amplitude-quantized Sampled Data Systems. AIEE Trans. (Applications and Industry) 81, 555–568 (1961)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Electrical & Computer Engineering, Concordia University, 1455 de Maisonneuve W., Montreal, Quebec, H3G 1M8, Canada

    Osman Hasan & Sofiène Tahar

Authors
  1. Osman Hasan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sofiène Tahar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Frank Pfenning

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hasan, O., Tahar, S. (2007). Formalization of Continuous Probability Distributions. In: Pfenning, F. (eds) Automated Deduction – CADE-21. CADE 2007. Lecture Notes in Computer Science(), vol 4603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73595-3_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-73595-3_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-73594-6

  • Online ISBN: 978-3-540-73595-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation