56183 20200221144342.0 doi 10.1186/s12859-016-1077-7 sideral 95339 ART-2016-95339 eng (orcid)0000-0001-5111-8357 Requeno, J.I. Universidad de Zaragoza Evaluation of properties over phylogenetic trees using stochastic logics 2016 Access copy available to the general public Unrestricted Background: 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. info:eu-repo/grantAgreement/ES/MINECO/TIN2013-40809-R info:eu-repo/semantics/openAccess by http://creativecommons.org/licenses/by/3.0/es/ 2.448 2016 MATHEMATICAL & COMPUTATIONAL BIOLOGY 10 / 57 = 0.175 2016 Q1 T1 BIOCHEMICAL RESEARCH METHODS 38 / 77 = 0.494 2016 Q2 T2 BIOTECHNOLOGY & APPLIED MICROBIOLOGY 67 / 160 = 0.419 2016 Q2 T2 1.581 2016 Applied Mathematics 2016 Q1 Biochemistry 2016 Q1 Computer Science Applications 2016 Q1 Molecular Biology 2016 Q2 Structural Biology 2016 Q2 info:eu-repo/semantics/article info:eu-repo/semantics/publishedVersion (orcid)0000-0001-5066-4030 Colom, J.M. Universidad de Zaragoza 5007 570 Universidad de Zaragoza Dpto. Informát.Ingenie.Sistms. Área Lenguajes y Sistemas Inf. 17, 1 (2016), 235 [14 pp] BMC bioinformatics BMC BIOINFORMATICS 1471-2105 1577353 http://zaguan.unizar.es/record/56183/files/texto_completo.pdf Versión publicada 10811 http://zaguan.unizar.es/record/56183/files/texto_completo.jpg?subformat=icon icon Versión publicada oai:zaguan.unizar.es:56183 articulos driver 2020-02-21-13:51:04 ARTICLE