| Abstract | Model checking is a generic veri cation technique that allows the phylogeneticist to focus on models and speci cations instead of on implementation issues. Phylogenetic trees are considered as transition
systems over which we interrogate phylogenetic questions written as formulas of temporal logic. Nonetheless, standard logics become insuficient for the usual practices of phylogenetic analysis since they don't allow the inclusion of explicit time and probabilities. The aim of this paper is to extend the application of model checking techniques beyond qualitative phylogenetic properties and adapt the existing logical extensions and tools to the eld of phylogeny. The introduction of time and probabilities in phylogenetic speci cations is motivated by a real example. |
