Requeno José Ignacio, Colom José Manuel
Department of Computer Science and Systems Engineering (DIIS), Universidad de Zaragoza, C/ María de Luna 1, 50018 Zaragoza, Spain.
J Integr Bioinform. 2014 Oct 23;11(3):248. doi: 10.2390/biecoll-jib-2014-248.
Model checking is a generic verification technique that allows the phylogeneticist to focus on models and specifications instead of on implementation issues. Phylogenetic trees are considered as transition systems over which we interrogate phylogenetic questions written as formulas of temporal logic. Nonetheless, standard logics become insufficient for certain practices of phylogenetic analysis since they do not allow the inclusion of explicit time and probabilities. The aim of this paper is to extend the application of model checking techniques beyond qualitative phylogenetic properties and adapt the existing logical extensions and tools to the field of phylogeny. The introduction of time and probabilities in phylogenetic specifications is motivated by the study of a real example: the analysis of the ratio of lactose intolerance in some populations and the date of appearance of this phenotype.
模型检查是一种通用的验证技术，它使系统发育学家能够专注于模型和规范，而不是实现问题。系统发育树被视为转换系统，我们可以在其上询问用时态逻辑公式表示的系统发育问题。然而，标准逻辑对于某些系统发育分析实践来说是不够的，因为它们不允许包含明确的时间和概率。本文的目的是将模型检查技术的应用扩展到定性系统发育属性之外，并使现有的逻辑扩展和工具适用于系统发育领域。在系统发育规范中引入时间和概率是由一个实际例子的研究推动的：对某些人群中乳糖不耐受的比例及其该表型出现日期的分析。
