Evaluation of properties over phylogenetic trees using stochastic logics

BMC Bioinformatics

Methodology Article

José Ignacio Requeno¹  José Manuel Colom¹ 

[1] Department of Computer Science and Systems Engineering (DIIS), Universidad de Zaragoza, C/ María de Luna 1, 50018, Zaragoza, Spain;

关键词: Phylogenetics;    Model checking;    Stochastic temporal logic;    DNA mutation models;    Maximum likelihood;   

DOI  :  10.1186/s12859-016-1077-7

 received in 2015-11-19, accepted in 2016-05-07,  发布年份 2016

来源: Springer

【 摘 要 】

BackgroundModel 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.ResultsIn 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.ConclusionsWe 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.

【 授权许可】

CC BY   
© Requeno and Colom. 2016

【 图 表 】

Fig. 2

Fig. 2

Fig. 2

Fig. 1

12951_2017_270_Article_IEq10.gif

Fig. 8

Fig. 3

Fig. 3

Fig. 7

12951_2015_111_Article_IEq5.gif

12951_2015_155_Article_IEq30.gif

Fig. 5

Fig. 6

12951_2017_270_Article_IEq9.gif

Fig. 2

12951_2017_270_Article_IEq8.gif

Fig. 1

12951_2015_111_Article_IEq4.gif

Fig. 1

13100_2023_302_Article_IEq7.gif

Fig. 2

Fig. 4

Fig. 5

12951_2015_155_Article_IEq28.gif

42004_2023_1020_Article_IEq18.gif

Fig. 3

Fig. 7

13100_2023_302_Article_IEq2.gif

13100_2023_302_Article_IEq1.gif

12951_2017_270_Article_IEq7.gif

42004_2023_1020_Article_IEq12.gif

Fig. 2

Fig. 7

Fig. 1

12951_2015_111_Article_IEq2.gif

12951_2015_155_Article_IEq25.gif

12951_2015_155_Article_IEq24.gif

Fig. 1