Model checking software for phylogenetic trees using distribution and database methods.

Area of Science:

• Computational Biology
• Bioinformatics
• Formal Methods

Background:

• Model checking, a formal verification paradigm from computer science, has been adapted for studying emergent biological properties on phylogenetic trees.
• Existing model checking approaches face performance limitations when applied to large-scale phylogenetic analyses due to computational complexity.

Purpose of the Study:

• To enhance the scalability and efficiency of model checking for analyzing biological properties on large phylogenetic trees.
• To present novel strategies for overcoming the performance bottlenecks of traditional model checking in phylogenetics.

Main Methods:

• Partitioning large phylogenetic trees into smaller, manageable subgraphs for distributed verification.
• Decoupling state-specific information (e.g., DNA sequences) from the phylogenetic tree and exporting it to external large-scale data management systems.

Main Results:

• The proposed strategies significantly improve computation time and memory consumption compared to monolithic model checking.
• Successful verification of properties on a real-world phylogenetic tree was achieved, demonstrating practical applicability.
• The integrated approach enhances the performance of model checking for complex biological systems.

Conclusions:

• The developed strategies effectively address the scalability challenges of model checking in phylogenetics.
• This approach enables the efficient verification of biological properties on large and complex phylogenetic datasets.
• Integration of partitioning and external data management offers a robust solution for computational phylogenetics.