This Article 
 Bibliographic References 
 Add to: 
Temporal Logics for Phylogenetic Analysis via Model Checking
July-Aug. 2013 (vol. 10 no. 4)
pp. 1058-1070
Jose Ignacio Requeno, Dept. Inf. e Ing. de Sist., Univ. de Zaragoza, Zaragoza, Spain
Gregorio De Miguel Casado, Dept. Inf. e Ing. de Sist., Univ. de Zaragoza, Zaragoza, Spain
Roberto Blanco, Dept. Inf. e Ing. de Sist., Univ. de Zaragoza, Zaragoza, Spain
Jose Manuel Colom, Dept. Inf. e Ing. de Sist., Univ. de Zaragoza, Zaragoza, Spain
The need for general-purpose algorithms for studying biological properties in phylogenetics motivates research into formal verification frameworks. Researchers can focus their efforts exclusively on evolution trees and property specifications. To this end, model checking, a mature automated verification technique originating in computer science, is applied to phylogenetic analysis. Our approach is based on three cornerstones: a logical modeling of the evolution with transition systems; the specification of both phylogenetic properties and trees using flexible temporal logic formulas; and the verification of the latter by means of automated computer tools. The most conspicuous result is the inception of a formal framework which allows for a symbolic manipulation of biological data (based on the codification of the taxa). Additionally, different logical models of evolution can be considered, complex properties can be specified in terms of the logical composition of others, and the refinement of unfulfilled properties as well as the discovery of new properties can be undertaken by exploiting the verification results. Some experimental results using a symbolic model verifier support the feasibility of the approach.
Index Terms:
temporal logic,biology computing,evolution (biological),formal verification,genetics,symbol manipulation,symbolic model verifier,temporal logics,phylogenetic analysis,model checking,general-purpose algorithms,biological properties,formal verification frameworks,evolution trees,property specifications,mature automated verification technique,logical modeling,flexible temporal logic formulas,automated computer tools,symbolic manipulation,biological data,logical models,Phylogeny,Model checking,Biological system modeling,Computational modeling,model checking,Phylogenetic analysis,formal verification,temporal logic
Jose Ignacio Requeno, Gregorio De Miguel Casado, Roberto Blanco, Jose Manuel Colom, "Temporal Logics for Phylogenetic Analysis via Model Checking," IEEE/ACM Transactions on Computational Biology and Bioinformatics, vol. 10, no. 4, pp. 1058-1070, July-Aug. 2013, doi:10.1109/TCBB.2013.87
Usage of this product signifies your acceptance of the Terms of Use.