Temporal logics for phylogenetic analysis via model checking

The need for general-purpose algorithms for the study of biological properties in phylogenetics motivates the research in formal verification frameworks so that researchers can focus their efforts exclusively on evolution modelling and property specification. To this end, model checking, a mature automated verification technique from computer science, is proposed for phylogenetic analysis. Three cornerstones found our approach: modelling evolution dynamics with transition systems; specifying phylogenetic properties using temporal logic formulae; and verifying the latter by means of automated computer tools. As prominent advantages stemming of studying phylogenetic properties with this approach, different models of evolution can be considered, complex properties can be specified as the logical composition of others, and the refinement of unfulfilled properties as well as the discovery of new ones can be undertaken by exploiting the verification results.