Login | Register

Formalization of the Standard Uniform random variable


Formalization of the Standard Uniform random variable

Hasan, Osman and Tahar, Sofiène (2007) Formalization of the Standard Uniform random variable. Theoretical Computer Science, 382 (1). pp. 71-83. ISSN 03043975

PDF - Accepted Version

Official URL: http://dx.doi.org/10.1016/j.tcs.2007.05.009


Continuous randomvariables are widely used to mathematically describe random phenomena in engineering and the physical sciences. In this paper, we present a higher-order logic formalization of the StandardUniformrandomvariable as the limit value of the sequence of its discrete approximations. We then show the correctness of this specification by proving the corresponding probability distribution properties within the HOL theorem prover, summarizing the proof steps. The formalized StandardUniformrandomvariable can be transformed to formalize other continuous randomvariables, such as Uniform, Exponential, Normal, etc., by using various non-uniformrandom number generation techniques. The formalization of these continuous randomvariables will enable us to perform an error free probabilistic analysis of systems within the framework of a higher-order-logic (HOL) theorem prover. For illustration purposes, we present the formalization of the Continuous Uniformrandomvariable based on the formalized StandardUniformrandomvariable, and then utilize it to perform a simple probabilistic analysis of roundoff error in HOL.

Divisions:Concordia University > Faculty of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Authors:Hasan, Osman and Tahar, Sofiène
Journal or Publication:Theoretical Computer Science
ID Code:974501
Deposited On:31 Jul 2012 20:08
Last Modified:31 Jul 2012 20:08
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

Back to top Back to top