Formal analysis of fault tree using probabilistic model checking: A solar array case study

Author(s):  
Marwan Ammar ◽  
Khaza Anuarul Hoque ◽  
Otmane Ait Mohamed
2014 ◽  
Vol 11 (3) ◽  
pp. 17-31 ◽  
Author(s):  
José Ignacio Requeno ◽  
José Manuel Colom

Summary Model checking is a generic verification technique that allows the phylogeneticist to focus on models and specifications instead of on implementation issues. Phylogenetic trees are considered as transition systems over which we interrogate phylogenetic questions written as formulas of temporal logic. Nonetheless, standard logics become insufficient for certain practices of phylogenetic analysis since they do not allow the inclusion of explicit time and probabilities. The aim of this paper is to extend the application of model checking techniques beyond qualitative phylogenetic properties and adapt the existing logical extensions and tools to the field of phylogeny. The introduction of time and probabilities in phylogenetic specifications is motivated by the study of a real example: the analysis of the ratio of lactose intolerance in some populations and the date of appearance of this phenotype.


Sign in / Sign up

Export Citation Format

Share Document