Login | Register

Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables

Title:

Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables

Hasan, Osman and Tahar, Sofiène (2008) Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. Journal of Automated Reasoning, 41 (3-4). pp. 295-323. ISSN 0168-7433

[thumbnail of using_theorem_proving_to_verify_expectation.pdf]
Preview
Text (application/pdf)
using_theorem_proving_to_verify_expectation.pdf - Accepted Version
243kB

Official URL: http://dx.doi.org/10.1007/s10817-008-9113-6

Abstract

Statistical quantities, such as expectation (mean) and variance, play a vital role in the present age probabilistic analysis. In this paper, we present some formalization of expectation theory that can be used to verify the expectation and variance characteristics of discrete random variables within the HOL theorem prover. The motivation behind this is the ability to perform error free probabilistic analysis, which in turn can be very useful for the performance and reliability analysis of systems used in safety-critical domains, such as space travel, medicine and military. We first present a formal definition of expectation of a function of a discrete random variable. Building upon this definition, we formalize the mathematical concept of variance and verify some classical properties of expectation and variance in HOL. We then utilize these formal definitions to verify the expectation and variance characteristics of the Geometric random variable. In order to demonstrate the practical effectiveness of the formalization presented in this paper, we also present the probabilistic analysis of the Coupon Collector’s problem in HOL.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Hasan, Osman and Tahar, Sofiène
Journal or Publication:Journal of Automated Reasoning
Date:2008
Digital Object Identifier (DOI):10.1007/s10817-008-9113-6
ID Code:974506
Deposited By: ANDREA MURRAY
Deposited On:31 Jul 2012 20:22
Last Modified:18 Jan 2018 17:38
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

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top