Formal Probabilistic Analysis: A Higher-Order Logic Based Approach

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{HasanT10,
  author       = {Osman Hasan and
                  Sofi{\`{e}}ne Tahar},
  editor       = {Marc Frappier and
                  Uwe Gl{\"{a}}sser and
                  Sarfraz Khurshid and
                  R{\'{e}}gine Laleau and
                  Steve Reeves},
  title        = {Formal Probabilistic Analysis: {A} Higher-Order Logic Based Approach},
  booktitle    = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
                  {ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5977},
  pages        = {2--19},
  publisher    = {Springer},
  year         = {2010},
  url          = {https://doi.org/10.1007/978-3-642-11811-1\_2},
  doi          = {10.1007/978-3-642-11811-1\_2},
  timestamp    = {Fri, 09 Apr 2021 18:50:59 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/HasanT10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}