College Publications logo   College Publications title  
View Basket
Homepage Contact page
Academia Brasileira de Filosofia
Cadernos de Lógica e Computação
Cadernos de Lógica e Filosofia
Cahiers de Logique et d'Epistemologie
Communication, Mind and Language
Cuadernos de lógica, Epistemología y Lenguaje
Encyclopaedia of Logic
Historia Logicae
IfColog series in Computational Logic
IfColog Lecture series
IfColog Proceedings
Journal of Applied Logics - IfCoLog Journal
Editorial Board
Scope of the Journal
Forthcoming papers
Logics for New-Generation AI
Logic and Law
Logic and Semiotics
Logic PhDs
Logic, Methodology and Philosophy of Science
The Logica Yearbook
Neural Computing and Artificial Intelligence
The SILFS series
Studies in Logic
Studies in Talmudic Logic
Texts in Logic and Reasoning
Texts in Mathematics
Digital Downloads
Information for authors
About us
Search for Books

Forthcoming papers


Probabilistic Analysis of Dynamic Fault Trees using HOL Theorem Proving

Yassmeen Elderhalli, Waqar Ahmad, Osman Hasan, Sofiene Tahar

Dynamic Fault Trees (DFTs) is a widely used failure modeling technique
that allows capturing the dynamic failure characteristics of systems in a very
effective manner. Simulation and model checking have been traditionally used
for the probabilistic analysis of DFTs. Simulation is usually based on sampling
and thus its results are not guaranteed to be complete, whereas model checking
employs computer arithmetic and numerical algorithms to compute the exact
values of probabilities, which contain many round-off errors. Leveraging upon
the expressive and sound nature of higher-order-logic (HOL) theorem proving,
we propose, in this paper, a formalization of DFT gates and their probabilistic
behaviors as well as some of their simplification properties in HOL based on
the algebraic approach. This formalization would allow us to conduct the probabilistic
analysis of DFTs by verifying generic mathematical expressions about
their behavior in HOL. In particular, we formalize the AND, OR, Priority-AND,
Functional DEPendency, Hot SPare, Cold SPare and theWarm SPare gates and
also verify their corresponding probabilistic expressions in HOL. Moreover, we
formally verify an important property, Pr(X < Y ), using the Lebesgue integral
as this relationship allows us to reason about the probabilistic properties of
the Priority-AND gate and the Before operator in HOL theorem proving. We
also formalize the notion of conditional densities in order to formally verify the
probabilistic expressions of the Cold SPare and the Warm SPare gates. In order
to illustrate the usefulness of our for

© 2005–2022 College Publications / VFH webmaster