000162395 001__ 162395 000162395 005__ 20251017144549.0 000162395 0247_ $$2doi$$a10.1109/TCBB.2013.87 000162395 0248_ $$2sideral$$a84618 000162395 037__ $$aART-2013-84618 000162395 041__ $$aeng 000162395 100__ $$0(orcid)0000-0001-5111-8357$$aRequeno, J.I.$$uUniversidad de Zaragoza 000162395 245__ $$aTemporal logics for phylogenetic analysis via model checking 000162395 260__ $$c2013 000162395 5060_ $$aAccess copy available to the general public$$fUnrestricted 000162395 5203_ $$aThe 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. 000162395 536__ $$9info:eu-repo/grantAgreement/ES/DGA/B117-10$$9info:eu-repo/grantAgreement/ES/MEC/AP2008-03447$$9info:eu-repo/grantAgreement/ES/MICINN/TIN2011-27479-C04-01 000162395 540__ $$9info:eu-repo/semantics/openAccess$$aAll rights reserved$$uhttp://www.europeana.eu/rights/rr-f/ 000162395 590__ $$a1.536$$b2013 000162395 591__ $$aSTATISTICS & PROBABILITY$$b24 / 119 = 0.202$$c2013$$dQ1$$eT1 000162395 591__ $$aMATHEMATICS, INTERDISCIPLINARY APPLICATIONS$$b24 / 95 = 0.253$$c2013$$dQ2$$eT1 000162395 591__ $$aCOMPUTER SCIENCE, INTERDISCIPLINARY APPLICATIONS$$b45 / 101 = 0.446$$c2013$$dQ2$$eT2 000162395 591__ $$aBIOCHEMICAL RESEARCH METHODS$$b63 / 77 = 0.818$$c2013$$dQ4$$eT3 000162395 655_4 $$ainfo:eu-repo/semantics/article$$vinfo:eu-repo/semantics/acceptedVersion 000162395 700__ $$0(orcid)0000-0001-6443-3815$$aDe Miguel Casado, G.$$uUniversidad de Zaragoza 000162395 700__ $$aBlanco, R. 000162395 700__ $$0(orcid)0000-0001-5066-4030$$aColom, J.M.$$uUniversidad de Zaragoza 000162395 7102_ $$15007$$2570$$aUniversidad de Zaragoza$$bDpto. Informát.Ingenie.Sistms.$$cÁrea Lenguajes y Sistemas Inf. 000162395 773__ $$g10, 4 (2013), 1058-1070$$pIEEE/ACM trans. comput. biol. bioinform.$$tIEEE/ACM transactions on computational biology and bioinformatics$$x1545-5963 000162395 8564_ $$s489841$$uhttps://zaguan.unizar.es/record/162395/files/texto_completo.pdf$$yPostprint 000162395 8564_ $$s3234137$$uhttps://zaguan.unizar.es/record/162395/files/texto_completo.jpg?subformat=icon$$xicon$$yPostprint 000162395 909CO $$ooai:zaguan.unizar.es:162395$$particulos$$pdriver 000162395 951__ $$a2025-10-17-14:10:55 000162395 980__ $$aARTICLE