162395 20251017144549.0 doi 10.1109/TCBB.2013.87 sideral 84618 ART-2013-84618 eng Requeno, J.I. Universidad de Zaragoza (orcid)0000-0001-5111-8357 Temporal logics for phylogenetic analysis via model checking 2013 Access copy available to the general public Unrestricted 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. info:eu-repo/grantAgreement/ES/DGA/B117-10 info:eu-repo/grantAgreement/ES/MEC/AP2008-03447 info:eu-repo/grantAgreement/ES/MICINN/TIN2011-27479-C04-01 info:eu-repo/semantics/openAccess All rights reserved http://www.europeana.eu/rights/rr-f/ 1.536 2013 STATISTICS & PROBABILITY 24 / 119 = 0.202 2013 Q1 T1 MATHEMATICS, INTERDISCIPLINARY APPLICATIONS 24 / 95 = 0.253 2013 Q2 T1 COMPUTER SCIENCE, INTERDISCIPLINARY APPLICATIONS 45 / 101 = 0.446 2013 Q2 T2 BIOCHEMICAL RESEARCH METHODS 63 / 77 = 0.818 2013 Q4 T3 info:eu-repo/semantics/article info:eu-repo/semantics/acceptedVersion De Miguel Casado, G. Universidad de Zaragoza (orcid)0000-0001-6443-3815 Blanco, R. Colom, J.M. Universidad de Zaragoza (orcid)0000-0001-5066-4030 5007 570 Universidad de Zaragoza Dpto. Informát.Ingenie.Sistms. Área Lenguajes y Sistemas Inf. 10, 4 (2013), 1058-1070 IEEE/ACM trans. comput. biol. bioinform. IEEE/ACM transactions on computational biology and bioinformatics 1545-5963 489841 http://zaguan.unizar.es/record/162395/files/texto_completo.pdf Postprint 3234137 http://zaguan.unizar.es/record/162395/files/texto_completo.jpg?subformat=icon icon Postprint oai:zaguan.unizar.es:162395 articulos driver 2025-10-17-14:10:55 ARTICLE