000056183 001__ 56183 000056183 005__ 20200221144342.0 000056183 0247_ $$2doi$$a10.1186/s12859-016-1077-7 000056183 0248_ $$2sideral$$a95339 000056183 037__ $$aART-2016-95339 000056183 041__ $$aeng 000056183 100__ $$0(orcid)0000-0001-5111-8357$$aRequeno, J.I.$$uUniversidad de Zaragoza 000056183 245__ $$aEvaluation of properties over phylogenetic trees using stochastic logics 000056183 260__ $$c2016 000056183 5060_ $$aAccess copy available to the general public$$fUnrestricted 000056183 5203_ $$aBackground: Model checking has been recently introduced as an integrated framework for extracting information of the phylogenetic trees using temporal logics as a querying language, an extension of modal logics that imposes restrictions of a boolean formula along a path of events. The phylogenetic tree is considered a transition system modeling the evolution as a sequence of genomic mutations (we understand mutation as different ways that DNA can be changed), while this kind of logics are suitable for traversing it in a strict and exhaustive way. Given a biological property that we desire to inspect over the phylogeny, the verifier returns true if the specification is satisfied or a counterexample that falsifies it. However, this approach has been only considered over qualitative aspects of the phylogeny. Results: In this paper, we repair the limitations of the previous framework for including and handling quantitative information such as explicit time or probability. To this end, we apply current probabilistic continuous-time extensions of model checking to phylogenetics. We reinterpret a catalog of qualitative properties in a numerical way, and we also present new properties that couldn't be analyzed before. For instance, we obtain the likelihood of a tree topology according to a mutation model. As case of study, we analyze several phylogenies in order to obtain the maximum likelihood with the model checking tool PRISM. In addition, we have adapted the software for optimizing the computation of maximum likelihoods. Conclusions: We have shown that probabilistic model checking is a competitive framework for describing and analyzing quantitative properties over phylogenetic trees. This formalism adds soundness and readability to the definition of models and specifications. Besides, the existence of model checking tools hides the underlying technology, omitting the extension, upgrade, debugging and maintenance of a software tool to the biologists. A set of benchmarks justify the feasibility of our approach. 000056183 536__ $$9info:eu-repo/grantAgreement/ES/MINECO/TIN2013-40809-R 000056183 540__ $$9info:eu-repo/semantics/openAccess$$aby$$uhttp://creativecommons.org/licenses/by/3.0/es/ 000056183 590__ $$a2.448$$b2016 000056183 591__ $$aMATHEMATICAL & COMPUTATIONAL BIOLOGY$$b10 / 57 = 0.175$$c2016$$dQ1$$eT1 000056183 591__ $$aBIOCHEMICAL RESEARCH METHODS$$b38 / 77 = 0.494$$c2016$$dQ2$$eT2 000056183 591__ $$aBIOTECHNOLOGY & APPLIED MICROBIOLOGY$$b67 / 160 = 0.419$$c2016$$dQ2$$eT2 000056183 592__ $$a1.581$$b2016 000056183 593__ $$aApplied Mathematics$$c2016$$dQ1 000056183 593__ $$aBiochemistry$$c2016$$dQ1 000056183 593__ $$aComputer Science Applications$$c2016$$dQ1 000056183 593__ $$aMolecular Biology$$c2016$$dQ2 000056183 593__ $$aStructural Biology$$c2016$$dQ2 000056183 655_4 $$ainfo:eu-repo/semantics/article$$vinfo:eu-repo/semantics/publishedVersion 000056183 700__ $$0(orcid)0000-0001-5066-4030$$aColom, J.M.$$uUniversidad de Zaragoza 000056183 7102_ $$15007$$2570$$aUniversidad de Zaragoza$$bDpto. Informát.Ingenie.Sistms.$$cÁrea Lenguajes y Sistemas Inf. 000056183 773__ $$g17, 1 (2016), 235 [14 pp]$$pBMC bioinformatics$$tBMC BIOINFORMATICS$$x1471-2105 000056183 8564_ $$s1577353$$uhttps://zaguan.unizar.es/record/56183/files/texto_completo.pdf$$yVersión publicada 000056183 8564_ $$s10811$$uhttps://zaguan.unizar.es/record/56183/files/texto_completo.jpg?subformat=icon$$xicon$$yVersión publicada 000056183 909CO $$ooai:zaguan.unizar.es:56183$$particulos$$pdriver 000056183 951__ $$a2020-02-21-13:51:04 000056183 980__ $$aARTICLE