The Community for Technology Leaders
RSS Icon
Issue No.04 - July-Aug. (2013 vol.10)
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.
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
[1] A.O. Mooers and S.B. Heard, "Inferring Evolutionary Process from Phylogenetic Tree Shape," Quarterly Rev. of Biology, vol. 72, pp. 31-54, 1997.
[2] E.S. Allman and J.A. Rhodes, "Trees, Fast and Accurate." Science, vol. 327, no. 5971, pp. 1334-1335, 2010.
[3] J. Felsenstein, Inferring Phylogenies. Sinauer, 2003.
[4] Z. Yang and B. Rannala, "Molecular Phylogenetics: Principles and Practice," Nature Rev. Genetics, vol. 13, no. 5, pp. 303-314, 2012.
[5] W.M. Fitch, "Uses for Evolutionary Trees," Philosophical Trans. Royal Soc. of London. Series B: Biological Sciences, vol. 349, no. 1327, pp. 93-102, 1995.
[6] O. Grumberg et al., 25 Years of Model Checking: History, Achievements, Perspectives. Springer, 2008.
[7] J. Barnat, L. Brim, A.A. Krejci, A. Streck, D. Safranek, M. Vejnar, and T. Vejpustek, "On Parameter Synthesis by Parallel Model Checking," IEEE/ACM Trans. Computational Biology and Bioinformatics, vol. 9, no. 3, pp. 693-705, May-June 2012.
[8] P.T. Monteiro, D. Ropers, R. Mateescu, A.T. Freitas, and H. Jong, "Temporal Logic Patterns for Querying Dynamic Models of Cellular Interaction Networks," Bioinformatics, vol. 24, pp. i227-i233, 2008.
[9] A. Rizk, G. Batt, F. Fages, and S. Soliman, "On a Continuous Degree of Satisfaction of Temporal Logic Formulae with Applications to Systems Biology," Proc. Sixth Int'l Conf. Computational Methods in Systems Biology, pp. 251-268, 2008.
[10] C.J. Langmead and S.K. Jha, "Predicting Protein Folding Kinetics via Temporal Logic Model Checking," Proc. Seventh Workshop Algorithms in Bioinformatics, pp. 252-264, 2007.
[11] E. De Maria, F. Fages, A. Rizk, and S. Soliman, "Design, Optimization and Predictions of a Coupled Model of the Cell Cycle, Circadian Clock, DNA Repair System, Irinotecan Metabolism and Exposure Control under Temporal Logic Constraints," Theoretical Computer Science, vol. 412, no. 21, pp. 2108-2127, 2011.
[12] R. Blanco, G. de Miguel Casado, J.I Requeno, and J.M. Colom, "Temporal Logics for Phylogenetic Analysis via Model Checking," Proc. IEEE Int'l Workshop Mining and Management of Biological and Health Data, 2010.
[13] J.I. Requeno, R. Blanco, G. de Miguel Casado, and J.M. Colom, "Phylogenetic Analysis Using an SMV Tool," Proc. Fifth Int'l Conf. Practical Applications of Computational Biology and Bioinformatics, pp. 167-174, 2011.
[14] C. Baier and J.-P. Katoen, Principles of Model Checking. MIT Press, 2008.
[15] E.M. Clarke and E.A. Emerson, "Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic," Proc. Workshop Logics of Programs, pp. 52-71, 1981.
[16] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, vol. C-35, no. 8, pp. 677-691, Aug. 1986.
[17] E. Paradis, Analysis of Phylogenetics and Evolution with R (Use R!), R. Gentleman et al., eds. Springer, 2012.
[18] W.P. Maddison and D. Maddison, "Mesquite: A Modular System for Evolutionary Analysis. Version 2.75," 2011.
[19] R. Knight et al., "PyCogent: A Toolkit for Making Sense from Sequence," Genome Biology, vol. 8, pp. 1-16, 2007.
[20] M.B. Richards, V.A. Macaulay, H.-J. Bandelt, and B.C. Sykes, "Phylogeography of Mitochondrial DNA in Western Europe," Annals of Human Genetics, vol. 62, pp. 241-260, 1998.
[21] E.O. Wiley, Phylogenetics: The Theory and Practice of Phylogenetic Systematics. Wiley, 1981.
[22] O. Lichtenstein, A. Pnueli, and L.D. Zuck, "The Glory of the Past," Proc. Conf. Logic of Programs, pp. 196-218, 1985.
[23] J. Montoya, E. López Gallardo, C.D. Sánchez, M.J. López Pérez, and E.R. Pesini, "20 Years of Human mtDNA Pathologic Point Mutations: Carefully Reading the Pathogenicity Criteria," Biochimica et Biophysica Acta, vol. 1787, pp. 476-483, 2009.
[24] A. Cimatti et al., "NuSMV 2: An OpenSource Tool for Symbolic Model Checking," Proc. 14th Int'l Conf. Computer Aided Verification, pp. 241-268, 2002.
[25] K. Varpaaniemi, J. Halme, K. Hiekkanen, and T. Pyssysalo, "PROD Reference Manual," technical report, Espoo, Finland, Helsinki Univ. of Technology, Digital Systems Laboratory, 1995.
[26] G.J. Holzmann, "The Model Checker SPIN," IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279-295, May 1997.
[27] J. Barnat, L. Brim, M. Ceska, and P. Rockai, "DiVinE: Parallel Distributed Model Checker," Proc. Ninth Int'l Workshop Parallel and Distributed Methods in Verification and Second Int'l Workshop High Performance Computational Systems Biology, pp. 4-7, 2010.
[28] I. Melatti et al., "Parallel and Distributed Model Checking in Eddy," Int'l J. Software Tools for Technology Transfer, vol. 11, no. 1, pp. 13-25, 2009.
[29] M. AlTurki and J. Meseguer, "PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool," Proc. Fourth Int'l Conf. Algebra and Coalgebra in Computer Science, pp. 386-392, 2011.
[30] M. Kwiatkowska, G. Norman, and D. Parker, "PRISM 4.0: Verification of Probabilistic Real-Time Systems," Proc. 23rd Int'l Conf. Computer Aided Verification, pp. 585-591, 2011.
[31] G. Behrmann, A. David, and K. Larsen, "A Tutorial on Uppaal," Formal Methods for the Design of Real-Time Systems, M. Bernardo et al., eds., pp. 33-35, Springer, 2004.
[32] M. Chechik and A. Gurfinkel, "TLQSolver: A Temporal Logic Query Checker," Proc. Int'l Conf. Computer Aided Verification, pp. 210-214, 2003.
[33] D. Robinson and L.R. Foulds, "Comparison of Phylogenetic Trees," Math. Biosciences, vol. 53, no. 1, pp. 131-147, 1981.
[34] M. Stich and S. Manrubia, "Topological Properties of Phylogenetic Trees in Evolutionary Models," European Physical J. B, vol. 70, no. 4, pp. 583-592, 2009.
[35] S.-J. Sul, S. Matthews, and T.L. Williams, "Using Tree Diversity to Compare Phylogenetic Heuristics," BMC Bioinformatics, vol. 10, no. Suppl 4, article S3, 2009.
[36] R. Alur and T. Henzinger, "Logics and Models of Real Time: A Survey," Proc. Real-Time: Theory in Practice, REX Workshop, pp. 74-106, 1992,
[37] S. Campos, E. Clarke, W. Marrero, M. Minea, and H. Hiraishi, "Computing Quantitative Characteristics of Finite-State Real-Time Systems," Proc. Real-Time Systems Symp., pp. 266-270, 1994.
[38] E. Emerson and R. Trefler, "Parametric Quantitative Temporal Reasoning," Proc. IEEE 14th Symp. Logic in Computer Science, pp. 336-343, 1999.
[39] S.K. Jha, E.M. Clarke, C.J. Langmead, A. Legay, A. Platzer, and P. Zuliani, "A Bayesian Approach to Model Checking Biological Systems," Proc. Seventh Int'l Conf. Computational Methods in Systems Biology, pp. 218-234, 2009.
[40] R. Segala and N. Lynch, "Probabilistic Simulations for Probabilistic Processes," Proc. Int'l Conf. Concurrency Theory, pp. 481-496, 1994.
[41] S. Donatelli, S. Haddad, and J. Sproston, "Model Checking Timed and Stochastic Properties with ${\rm CSL}^{\rm ta}$ ," IEEE Trans. Software Eng., vol. 35, no. 2, pp. 224-240, Mar./Apr. 2009.
[42] Z. Yang, Computational Molecular Evolution, P. Harvey and R.M. May, eds. Oxford Univ. Press, 2006.
[43] W. Chan, "Temporal-Logic Queries," Proc. 12th Conf. Computer Aided Verification, pp. 450-463, 2000.
[44] A. Gurfinkel, M. Chechik, and B. Devereux, "Temporal Logic Query Checking: A Tool for Model Exploration," IEEE Trans. Software Eng., vol. 29, no. 10, pp. 898-914, Oct. 2003.
[45] J.I. Requeno, R. Blanco, G. de Miguel Casado, and J.M. Colom, "Sliced Model Checking for Phylogenetic Analysis," Proc. Sixth Int'l Conf. Practical Applications of Computational Biology and Bioinformatics, pp. 95-103, 2012.
[46] J.I. Requeno and J.M. Colom, "Speeding Up Phylogenetic Model Checking," Proc. Seventh Int'l Conf. Practical Applications of Computational Biology and Bioinformatics, pp. 119-126, 2013.
[47] G. Bhat, R. Cleaveland, and O. Grumberg, "Efficient On-the-Fly Model Checking for CTL," Proc. IEEE Tenth Symp. Logic in Computer Science, pp. 388-397, 1995.
[48] J.E. Stajich et al., "The Bioperl Toolkit: Perl Modules for the Life Sciences," Genome Research, vol. 12, no. 10, pp. 1611-1618, 2002.
[49] D.A. Benson et al., "GenBank," Nucleic Acids Research, vol. 40, no. D1, pp. D48-D53, 2012.
[50] D.H. Huson et al., Phylogenetic Networks: Concepts, Algorithms and Applications, Cambridge Univ. Press, 2011.
[51] A.P. Stamatakis, T. Ludwig, and H. Meier, "The AxML Program Family for Maximum Likelihood-Based Phylogenetic Tree Inference," Concurrency and Computation: Practice and Experience, vol. 16, no. 9, pp. 975-988, 2004.
68 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool