Requeno José Ignacio, Colom José Manuel
Department of Computer Science and Systems Engineering (DIIS), Universidad de Zaragoza, C/ María de Luna 1, Zaragoza, 50018, Spain.
BMC Bioinformatics. 2016 Jun 14;17(1):235. doi: 10.1186/s12859-016-1077-7.
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.
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.
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.
模型检查最近被引入作为一个集成框架，用于使用时态逻辑作为查询语言来提取系统发育树的信息，时态逻辑是模态逻辑的一种扩展，它沿着事件路径对布尔公式施加限制。系统发育树被视为一个转换系统，将进化建模为基因组突变的序列（我们将突变理解为DNA可以被改变的不同方式），而这种逻辑适合以严格且详尽的方式遍历它。给定一个我们希望在系统发育中检查的生物学特性，如果规范得到满足，验证器返回真，否则返回一个证伪它的反例。然而，这种方法仅考虑了系统发育的定性方面。
在本文中，我们修复了先前框架在包含和处理定量信息（如显式时间或概率）方面的局限性。为此，我们将模型检查的当前概率连续时间扩展应用于系统发育学。我们以数值方式重新解释了一系列定性属性，并且还提出了以前无法分析的新属性。例如，我们根据突变模型获得树拓扑的似然性。作为案例研究，我们分析了几个系统发育树，以便使用模型检查工具PRISM获得最大似然性。此外，我们对软件进行了调整，以优化最大似然性的计算。
我们已经表明，概率模型检查是用于描述和分析系统发育树上定量属性的一个有竞争力的框架。这种形式主义为模型和规范的定义增加了合理性和可读性。此外，模型检查工具的存在隐藏了底层技术，为生物学家省去了软件工具的扩展、升级、调试和维护。一组基准证明了我们方法的可行性。
