Temporal logics for phylogenetic analysis via model checking

IEEE/ACM Transactions on Computational Biology and Bioinformatics
José Ignacio RequenoJosé Manuel Colom

Abstract

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.

References

Jul 29, 1995·Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences·W M Fitch
Nov 6, 1998·Annals of Human Genetics·M B RichardsB C Sykes
Oct 9, 2002·Genome Research·Jason E StajichEwan Birney
Aug 22, 2007·Genome Biology·Rob KnightGavin A Huttley
Aug 12, 2008·Bioinformatics·Pedro T MonteiroHidde de Jong
Oct 9, 2008·Biochimica Et Biophysica Acta·Julio MontoyaEduardo Ruiz-Pesini
May 14, 2009·BMC Bioinformatics·Seung-Jin SulTiffani L Williams
Mar 13, 2010·Science·Elizabeth S Allman, John A Rhodes
Jul 27, 2011·IEEE/ACM Transactions on Computational Biology and Bioinformatics·Jirí BarnatTomás Vejpustek
Dec 7, 2011·Nucleic Acids Research·Dennis A BensonEric W Sayers
Mar 30, 2012·Nature Reviews. Genetics·Ziheng Yang, Bruce Rannala

❮ Previous
Next ❯

Citations

Jun 16, 2016·BMC Bioinformatics·José Ignacio Requeno, José Manuel Colom

❮ Previous
Next ❯

Related Concepts

Trending Feeds

COVID-19

Coronaviruses encompass a large family of viruses that cause the common cold as well as more serious diseases, such as the ongoing outbreak of coronavirus disease 2019 (COVID-19; formally known as 2019-nCoV). Coronaviruses can spread from animals to humans; symptoms include fever, cough, shortness of breath, and breathing difficulties; in more severe cases, infection can lead to death. This feed covers recent research on COVID-19.

Blastomycosis

Blastomycosis fungal infections spread through inhaling Blastomyces dermatitidis spores. Discover the latest research on blastomycosis fungal infections here.

Nuclear Pore Complex in ALS/FTD

Alterations in nucleocytoplasmic transport, controlled by the nuclear pore complex, may be involved in the pathomechanism underlying multiple neurodegenerative diseases including Amyotrophic Lateral Sclerosis and Frontotemporal Dementia. Here is the latest research on the nuclear pore complex in ALS and FTD.

Applications of Molecular Barcoding

The concept of molecular barcoding is that each original DNA or RNA molecule is attached to a unique sequence barcode. Sequence reads having different barcodes represent different original molecules, while sequence reads having the same barcode are results of PCR duplication from one original molecule. Discover the latest research on molecular barcoding here.

Chronic Fatigue Syndrome

Chronic fatigue syndrome is a disease characterized by unexplained disabling fatigue; the pathology of which is incompletely understood. Discover the latest research on chronic fatigue syndrome here.

Evolution of Pluripotency

Pluripotency refers to the ability of a cell to develop into three primary germ cell layers of the embryo. This feed focuses on the mechanisms that underlie the evolution of pluripotency. Here is the latest research.

Position Effect Variegation

Position Effect Variagation occurs when a gene is inactivated due to its positioning near heterochromatic regions within a chromosome. Discover the latest research on Position Effect Variagation here.

STING Receptor Agonists

Stimulator of IFN genes (STING) are a group of transmembrane proteins that are involved in the induction of type I interferon that is important in the innate immune response. The stimulation of STING has been an active area of research in the treatment of cancer and infectious diseases. Here is the latest research on STING receptor agonists.

Microbicide

Microbicides are products that can be applied to vaginal or rectal mucosal surfaces with the goal of preventing, or at least significantly reducing, the transmission of sexually transmitted infections. Here is the latest research on microbicides.