Evaluation of properties over phylogenetic trees using stochastic logics

Area of Science:

• Computational Biology
• Evolutionary Biology
• Formal Methods

Background:

• Model checking, using temporal logics, has been applied to phylogenetic trees for qualitative information extraction.
• Previous methods were limited to qualitative aspects, lacking the ability to handle quantitative data like time or probability.

Purpose of the Study:

• To extend phylogenetic model checking to incorporate and analyze quantitative information, such as time and probability.
• To develop new methods for analyzing properties not previously addressable in phylogenetic analysis.

Main Methods:

• Applied probabilistic continuous-time extensions of model checking to phylogenetics.
• Reinterpreted qualitative properties into a numerical framework.
• Utilized the PRISM model checking tool for analyzing phylogenies and computing maximum likelihoods.
• Adapted software for optimizing maximum likelihood computations.

Main Results:

• Successfully incorporated quantitative information (time, probability) into phylogenetic model checking.
• Enabled the analysis of new, quantitative properties, including the likelihood of tree topologies under mutation models.
• Achieved optimized computation of maximum likelihoods for phylogenetic trees using the PRISM tool.

Conclusions:

• Probabilistic model checking offers a robust and readable framework for quantitative analysis of phylogenetic trees.
• The use of model checking tools simplifies complex computational aspects for biologists.
• The approach is demonstrated to be feasible and effective through benchmark analyses.