Sciweavers

Share
FM
2009
Springer

Formal Reasoning about Expectation Properties for Continuous Random Variables

9 years 6 months ago
Formal Reasoning about Expectation Properties for Continuous Random Variables
Abstract. Expectation (average) properties of continuous random variables are widely used to judge performance characteristics in engineering and physical sciences. This paper presents an infrastructure that can be used to formally reason about expectation properties of most of the continuous random variables in a theorem prover. Starting from the relatively complex higher-order-logic definition of expectation, based on Lebesgue integration, we formally verify key expectation properties that allow us to reason about expectation of a continuous random variable in terms of simple arithmetic operations. In order to illustrate the practical effectiveness and utilization of our approach, we also present the formal verification of expectation properties of the commonly used continuous random variables: Uniform, Triangular and Exponential.
Osman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofi&
Added 24 Jul 2010
Updated 24 Jul 2010
Type Conference
Year 2009
Where FM
Authors Osman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofiène Tahar, Reza Akbarpour
Comments (0)
books