University of Zaragoza, Zaragoza.
IEEE/ACM Trans Comput Biol Bioinform. 2013 Jul-Aug;10(4):1058-70. doi: 10.1109/TCBB.2013.87.
The need for general-purpose algorithms for studying biological properties in phylogenetics motivates research into formal verification frameworks. Researchers can focus their efforts exclusively on evolution trees and property specifications. To this end, model checking, a mature automated verification technique originating in computer science, is applied to phylogenetic analysis. Our approach is based on three cornerstones: a logical modeling of the evolution with transition systems; the specification of both phylogenetic properties and trees using flexible temporal logic formulas; and the verification of the latter by means of automated computer tools. The most conspicuous result is the inception of a formal framework which allows for a symbolic manipulation of biological data (based on the codification of the taxa). Additionally, different logical models of evolution can be considered, complex properties can be specified in terms of the logical composition of others, and the refinement of unfulfilled properties as well as the discovery of new properties can be undertaken by exploiting the verification results. Some experimental results using a symbolic model verifier support the feasibility of the approach.
在系统发生学中研究生物特性需要通用算法，这促使人们研究形式验证框架。研究人员可以专门专注于进化树和属性规范。为此，模型检查，一种源自计算机科学的成熟自动化验证技术，被应用于系统发生分析。我们的方法基于三个基石：使用转换系统对进化进行逻辑建模；使用灵活的时态逻辑公式对系统发生属性和树进行规范；以及通过自动化计算机工具验证后者。最显著的结果是引入了一个形式框架，允许对生物数据进行符号操作（基于分类单元的编码）。此外，可以考虑不同的进化逻辑模型，可以根据其他逻辑组合来规范复杂的属性，并且可以通过利用验证结果来细化未满足的属性以及发现新的属性。使用符号模型验证器的一些实验结果支持该方法的可行性。
