-
Osman Hasan and Sofi�ne Tahar.
Formal Verification of Tail Distribution Bounds in the HOL Theorem Prover.
Mathematical Methods in the Applied Sciences,
32(4):480-504,
March 2009.
ISSN: 01704214, 10991476.
Keyword(s): HOL,
probability.
Abstract:
|
Tail distribution bounds play a major role in the estimation of failure probabilities in performance and reliability analysis of systems. They are usually estimated using Markov's and Chebyshev's inequalities, which represent tail distribution bounds for a random variable in terms of its mean or variance. This paper presents the formal verification of Markov's and Chebyshev's inequalities for discrete random variables using a higher-order-logic theorem prover. The paper also provides the formal verification of mean and variance relations for some of the widely used discrete random variables, such as Uniform(m), Bernoulli( p), Geometric( p) and Binomial(m, p) random variables. This infrastructure allows us to precisely reason about the tail distribution properties and thus turns out to be quite useful for the analysis of systems used in safety-critical domains, such as space, medicine or transportation. For illustration purposes, we present the performance analysis of the coupon collector's problem, a well-known commercially used algorithm. Copyright q 2008 John Wiley \& Sons, Ltd. |
@article{hasanFormalVerificationTail2009,
title = {Formal Verification of Tail Distribution Bounds in the {{HOL}} Theorem Prover},
author = {Hasan, Osman and Tahar, Sofi{\`e}ne},
year = {2009},
month = mar,
volume = {32},
pages = {480--504},
issn = {01704214, 10991476},
doi = {10.1002/mma.1055},
abstract = {Tail distribution bounds play a major role in the estimation of failure probabilities in performance and reliability analysis of systems. They are usually estimated using Markov's and Chebyshev's inequalities, which represent tail distribution bounds for a random variable in terms of its mean or variance. This paper presents the formal verification of Markov's and Chebyshev's inequalities for discrete random variables using a higher-order-logic theorem prover. The paper also provides the formal verification of mean and variance relations for some of the widely used discrete random variables, such as Uniform(m), Bernoulli( p), Geometric( p) and Binomial(m, p) random variables. This infrastructure allows us to precisely reason about the tail distribution properties and thus turns out to be quite useful for the analysis of systems used in safety-critical domains, such as space, medicine or transportation. For illustration purposes, we present the performance analysis of the coupon collector's problem, a well-known commercially used algorithm. Copyright q 2008 John Wiley \& Sons, Ltd.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4308-Hasan_Tahar (2009) - Formal verification of tail distribution bounds in the HOL theorem prover.pdf},
journal = {Mathematical Methods in the Applied Sciences},
keywords = {HOL,probability},
number = {4}
}
-
Osman Hasan and Sofi�ne Tahar.
Probabilistic Analysis of Wireless Systems Using Theorem Proving.
Electronic Notes in Theoretical Computer Science,
242(2):43-58,
July 2009.
ISSN: 15710661.
Keyword(s): HOL,
probability.
Abstract:
|
Probabilistic techniques play a major role in the design and analysis of wireless systems as they contain a significant amount of random or unpredictable components. Traditionally, computer simulation techniques are used to perform probabilistic analysis of wireless systems but they provide inaccurate results and usually require enormous amount of CPU time in order to attain reasonable estimates. To overcome these limitations, we propose to use a higher-order-logic theorem prover (HOL) for the analysis of wireless systems. The paper presents a concise description of the formal foundations required to conduct the analysis of a wireless system in a theorem prover, such as the higher-order-logic modeling of random variables and the verification of their corresponding probabilistic and statistical properties in a theorem prover. In order to illustrate the utilization and effectiveness of the proposed idea for handling real-world wireless system analysis problems, we present an analysis of the automated repeat request (ARQ) mechanism at the logic link control (LLC) layer of the General Packet Radio Service (GPRS), which is a packet oriented mobile data service available to the users of Global System for Mobile Communications (GSM). |
@article{hasanProbabilisticAnalysisWireless2009,
title = {Probabilistic {{Analysis}} of {{Wireless Systems Using Theorem Proving}}},
author = {Hasan, Osman and Tahar, Sofi{\`e}ne},
year = {2009},
month = jul,
volume = {242},
pages = {43--58},
issn = {15710661},
doi = {10.1016/j.entcs.2009.06.022},
abstract = {Probabilistic techniques play a major role in the design and analysis of wireless systems as they contain a significant amount of random or unpredictable components. Traditionally, computer simulation techniques are used to perform probabilistic analysis of wireless systems but they provide inaccurate results and usually require enormous amount of CPU time in order to attain reasonable estimates. To overcome these limitations, we propose to use a higher-order-logic theorem prover (HOL) for the analysis of wireless systems. The paper presents a concise description of the formal foundations required to conduct the analysis of a wireless system in a theorem prover, such as the higher-order-logic modeling of random variables and the verification of their corresponding probabilistic and statistical properties in a theorem prover. In order to illustrate the utilization and effectiveness of the proposed idea for handling real-world wireless system analysis problems, we present an analysis of the automated repeat request (ARQ) mechanism at the logic link control (LLC) layer of the General Packet Radio Service (GPRS), which is a packet oriented mobile data service available to the users of Global System for Mobile Communications (GSM).},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4306-Hasan_Tahar (2009) - Probabilistic Analysis of Wireless Systems Using Theorem Proving.pdf},
journal = {Electronic Notes in Theoretical Computer Science},
keywords = {HOL,probability},
number = {2}
}
-
Favio Ezequiel Miranda-Perea.
Two Extensions of System F with (Co)Iteration and Primitive (Co)Recursion Principles.
RAIRO - Theoretical Informatics and Applications,
43(4):703-766,
October 2009.
ISSN: 0988-3754, 1290-385X.
Keyword(s): calculus,
coinduction.
Abstract:
|
This paper presents two extensions of the second order polymorphic lambda calculus, system F, with monotone (co)inductive types supporting (co)iteration, primitive (co)recursion and inversion principles as primitives. One extension is inspired by the usual categorical approach to programming by means of initial algebras and final coalgebras; whereas the other models dialgebras, and can be seen as an extension of Hagino's categorical lambda calculus within the framework of parametric polymorphism. The systems are presented in Curry-style, and are proven to be terminating and type-preserving. Moreover their expressiveness is shown by means of several programming examples, going from usual data types to lazy codata types such as streams or infinite trees. |
@article{miranda-pereaTwoExtensionsSystem2009,
title = {Two Extensions of System {{F}} with (Co)Iteration and Primitive (Co)Recursion Principles},
author = {{Miranda-Perea}, Favio Ezequiel},
year = {2009},
month = oct,
volume = {43},
pages = {703--766},
issn = {0988-3754, 1290-385X},
doi = {10.1051/ita/2009015},
abstract = {This paper presents two extensions of the second order polymorphic lambda calculus, system F, with monotone (co)inductive types supporting (co)iteration, primitive (co)recursion and inversion principles as primitives. One extension is inspired by the usual categorical approach to programming by means of initial algebras and final coalgebras; whereas the other models dialgebras, and can be seen as an extension of Hagino's categorical lambda calculus within the framework of parametric polymorphism. The systems are presented in Curry-style, and are proven to be terminating and type-preserving. Moreover their expressiveness is shown by means of several programming examples, going from usual data types to lazy codata types such as streams or infinite trees.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4382-Miranda-Perea (2009) - Two extensions of system F with (co)iteration and primitive (co)recursion.pdf},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {calculus,coinduction},
number = {4}
}