000162393 001__ 162393 000162393 005__ 20251017144548.0 000162393 0247_ $$2doi$$a10.1007/978-3-642-19914-1_23 000162393 0248_ $$2sideral$$a74082 000162393 037__ $$aART-2011-74082 000162393 041__ $$aeng 000162393 100__ $$0(orcid)0000-0001-5111-8357$$aRequeno, J.I. 000162393 245__ $$aPhylogenetic analysis using an SMV tool 000162393 260__ $$c2011 000162393 5060_ $$aAccess copy available to the general public$$fUnrestricted 000162393 5203_ $$aThe need for general methods to verify biological properties in phylogenetics motivates research in formal frameworks so that biologists can focus their efforts exclusively in evolution modeling and property specification. Model checking is proposed to this end. Three pillars found this approach: modeling evolution dynamics as transition systems; specifying phylogenetic properties using temporal logic formulae; and verifying the former by means of automated computer tools. As prominent advantages for studying biological properties under our approach, different models of evolution can be considered, complex properties can be specified as the logical composition of others, and the refinement of unfulfilled properties as well as the discovery of new ones can be undertaken by exploiting the results of verification. Preliminary experimental results using the Cadence Symbolic Model Verifier support the feasibility of the methodology. 000162393 536__ $$9info:eu-repo/grantAgreement/ES/DGA/B117-10$$9info:eu-repo/grantAgreement/ES/MEC/AP2008-03447$$9info:eu-repo/grantAgreement/ES/MICINN/TIN2008-06582-C03-02 000162393 540__ $$9info:eu-repo/semantics/openAccess$$aAll rights reserved$$uhttp://www.europeana.eu/rights/rr-f/ 000162393 655_4 $$ainfo:eu-repo/semantics/article$$vinfo:eu-repo/semantics/acceptedVersion 000162393 700__ $$aBlanco, R.$$uUniversidad de Zaragoza 000162393 700__ $$0(orcid)0000-0001-6443-3815$$aDe Miguel Casado, Gregorio$$uUniversidad de Zaragoza 000162393 700__ $$0(orcid)0000-0001-5066-4030$$aColom, J.M.$$uUniversidad de Zaragoza 000162393 7102_ $$15007$$2570$$aUniversidad de Zaragoza$$bDpto. Informát.Ingenie.Sistms.$$cÁrea Lenguajes y Sistemas Inf. 000162393 773__ $$g93 (2011), 167-174$$tAdvances in Intelligent and Soft Computing$$x1867-5662 000162393 8564_ $$s147292$$uhttps://zaguan.unizar.es/record/162393/files/texto_completo.pdf$$yPostprint 000162393 8564_ $$s1311555$$uhttps://zaguan.unizar.es/record/162393/files/texto_completo.jpg?subformat=icon$$xicon$$yPostprint 000162393 909CO $$ooai:zaguan.unizar.es:162393$$particulos$$pdriver 000162393 951__ $$a2025-10-17-14:10:46 000162393 980__ $$aARTICLE