返回
Temporal Logics for Phylogenetic Analysis via Model Checking
DOI:10.1109/TCBB.2013.87.png)
摘要
En 中文
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.
Keyword:
Phylogenetic analysis
formal verification
temporal logic
model checking
AI总结
对已上传原文的论文进行重点信息的提取,主要内容包括:简要概述、研究摘要、背景介绍、关键亮点、图文解析、展望与总结。
期刊
I
IF:
3.4
论文数:
3.3K
被引数:
6.4K
机构
引用论文
Effects of Mutations of Aspartic Acid 63 on the Metal-Binding Properties of the Recombinant N-Lobe of Human Serum Transferrin
Biochemistry
IF0

