{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T09:13:29Z","timestamp":1762506809163,"version":"3.37.3"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,6,14]],"date-time":"2016-06-14T00:00:00Z","timestamp":1465862400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2016,6,14]],"date-time":"2016-06-14T00:00:00Z","timestamp":1465862400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["BMC Bioinformatics"],"abstract":"<jats:title>Abstract<\/jats:title><jats:sec>\n                <jats:title>Background<\/jats:title>\n                <jats:p>Model checking has been recently introduced as an integrated framework for extracting information of the phylogenetic trees using temporal logics as a querying language, an extension of modal logics that imposes restrictions of a boolean formula along a path of events. The phylogenetic tree is considered a transition system modeling the evolution as a sequence of genomic mutations (we understand mutation as different ways that DNA can be changed), while this kind of logics are suitable for traversing it in a strict and exhaustive way. Given a biological property that we desire to inspect over the phylogeny, the verifier returns true if the specification is satisfied or a counterexample that falsifies it. However, this approach has been only considered over qualitative aspects of the phylogeny.<\/jats:p>\n              <\/jats:sec><jats:sec>\n                <jats:title>Results<\/jats:title>\n                <jats:p>In this paper, we repair the limitations of the previous framework for including and handling quantitative information such as explicit time or probability. To this end, we apply current probabilistic continuous-time extensions of model checking to phylogenetics. We reinterpret a catalog of qualitative properties in a numerical way, and we also present new properties that couldn\u2019t be analyzed before. For instance, we obtain the likelihood of a tree topology according to a mutation model. As case of study, we analyze several phylogenies in order to obtain the maximum likelihood with the model checking tool PRISM. In addition, we have adapted the software for optimizing the computation of maximum likelihoods.<\/jats:p>\n              <\/jats:sec><jats:sec>\n                <jats:title>Conclusions<\/jats:title>\n                <jats:p>We have shown that probabilistic model checking is a competitive framework for describing and analyzing quantitative properties over phylogenetic trees. This formalism adds soundness and readability to the definition of models and specifications. Besides, the existence of model checking tools hides the underlying technology, omitting the extension, upgrade, debugging and maintenance of a software tool to the biologists. A set of benchmarks justify the feasibility of our approach.<\/jats:p>\n              <\/jats:sec>","DOI":"10.1186\/s12859-016-1077-7","type":"journal-article","created":{"date-parts":[[2016,6,14]],"date-time":"2016-06-14T11:18:31Z","timestamp":1465903111000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Evaluation of properties over phylogenetic trees using stochastic logics"],"prefix":"10.1186","volume":"17","author":[{"given":"Jos\u00e9 Ignacio","family":"Requeno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9 Manuel","family":"Colom","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,14]]},"reference":[{"key":"1077_CR1","volume-title":"Inferring Phylogenies","author":"J Felsenstein","year":"2003","unstructured":"Felsenstein J, Vol. 2. Inferring Phylogenies. Sunderland, Massachusetts: Sinauer Associates; 2003."},{"issue":"5","key":"1077_CR2","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1038\/nrg3186","volume":"13","author":"Z Yang","year":"2012","unstructured":"Yang Z, Rannala B. Molecular phylogenetics: Principles and practice. Nat Rev Genet. 2012; 13(5):303\u201314.","journal-title":"Nat Rev Genet"},{"issue":"1327","key":"1077_CR3","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1098\/rstb.1995.0095","volume":"349","author":"WM Fitch","year":"1995","unstructured":"Fitch WM. Uses for evolutionary trees. Philos Trans R Soc Lond Series B Biol Sci. 1995; 349(1327):93\u2013102.","journal-title":"Philos Trans R Soc Lond Series B Biol Sci"},{"key":"1077_CR4","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1038\/ng1113","volume":"33","author":"LL Cavalli-Sforza","year":"2003","unstructured":"Cavalli-Sforza LL, Feldman MW. The application of molecular genetic approaches to the study of human evolution. Nat Genet. 2003; 33:266\u201375.","journal-title":"Nat Genet"},{"issue":"5\/6","key":"1077_CR5","doi-asserted-by":"publisher","first-page":"597","DOI":"10.3378\/027.081.0609","volume":"81","author":"C Holden","year":"2009","unstructured":"Holden C, Mace R. Phylogenetic analysis of the evolution of lactose digestion in adults. Hum Biol. 2009; 81(5\/6):597\u2013619.","journal-title":"Hum Biol"},{"issue":"21","key":"1077_CR6","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1086\/419657","volume":"72","author":"AO Mooers","year":"1997","unstructured":"Mooers AO, Heard SB. Inferring evolutionary process from phylogenetic tree shape. Q Rev Biol. 1997; 72(21):31\u201354.","journal-title":"Q Rev Biol"},{"key":"1077_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0","volume-title":"25 Years of model checking: history, achievements, perspectives","author":"O Grumberg","year":"2008","unstructured":"Grumberg O, Veith H. 25 Years of model checking: history, achievements, perspectives. Berlin: Springer; 2008."},{"issue":"4","key":"1077_CR8","doi-asserted-by":"publisher","first-page":"1058","DOI":"10.1109\/TCBB.2013.87","volume":"10","author":"JI Requeno","year":"2013","unstructured":"Requeno JI, de Miguel Casado G, Blanco R, Colom JM. Temporal logics for phylogenetic analysis via model checking. IEEE\/ACM Trans Comput Biol Bioinform. 2013; 10(4):1058\u201370.","journal-title":"IEEE\/ACM Trans Comput Biol Bioinform"},{"key":"1077_CR9","unstructured":"Requeno JI. Formal methods applied to the analysis of phylogenies: Phylogenetic Model Checking PhD thesis: School of Engineering and Architecture, University of Zaragoza; 2014."},{"key":"1077_CR10","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P. Principles of model checking. Cambridge, Massachusetts: The MIT Press; 2008."},{"issue":"2","key":"1077_CR11","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst (TOPLAS). 1986; 8(2):244\u201363.","journal-title":"ACM Trans Program Lang Syst (TOPLAS)"},{"issue":"3","key":"1077_CR12","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1515\/jib-2014-248","volume":"11","author":"JI Requeno","year":"2014","unstructured":"Requeno JI, Colom JM. Analyzing phylogenetic trees with timed and probabilistic model checking: The lactose persistence case study. J Integr Bioinform. 2014; 11(3):248.","journal-title":"J Integr Bioinform"},{"issue":"5","key":"1077_CR13","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson H, Jonsson B. A logic for reasoning about time and reliability. Form Asp Comput. 1994; 6(5):512\u201335.","journal-title":"Form Asp Comput"},{"issue":"2","key":"1077_CR14","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1109\/TSE.2008.108","volume":"35","author":"S Donatelli","year":"2009","unstructured":"Donatelli S, Haddad S, Sproston J. Model checking timed and stochastic properties with CSLTA. IEEE Trans Softw Eng. 2009; 35(2):224\u201340.","journal-title":"IEEE Trans Softw Eng"},{"issue":"3","key":"1077_CR15","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/s11704-013-2195-2","volume":"7","author":"S Konur","year":"2013","unstructured":"Konur S. A survey on temporal logics for specifying and verifying real-time systems. Frontiers of Computer Science. 2013; 7(3):370\u2013403. doi:10.1007\/s11704-013-2195-2. http:\/\/dx.doi.org\/10.1007\/s11704-013-2195-2","journal-title":"Frontiers of Computer Science"},{"key":"1077_CR16","unstructured":"Lewis P, Holder M, Swofford D. Phycas: software for phylogenetic analysis: Storrs, CT: University of Connecticut; 2008. See www.phycas.org."},{"issue":"5","key":"1077_CR17","doi-asserted-by":"publisher","first-page":"753","DOI":"10.1093\/sysbio\/syu039","volume":"63","author":"S H\u00f6hna","year":"2014","unstructured":"H\u00f6hna S, Heath TA, Boussau B, Landis MJ, Ronquist F, Huelsenbeck JP. Probabilistic graphical model representation in phylogenetics. Syst Biol. 2014; 63(5):753\u201371.","journal-title":"Syst Biol"},{"issue":"4","key":"1077_CR18","doi-asserted-by":"publisher","first-page":"1003537","DOI":"10.1371\/journal.pcbi.1003537","volume":"10","author":"R Bouckaert","year":"2014","unstructured":"Bouckaert R, Heled J, K\u00fchnert D, Vaughan T, Wu CH, Xie D, Suchard MA, Rambaut A, Drummond AJ. Beast 2: a software platform for bayesian evolutionary analysis. PLoS Comput Biol. 2014; 10(4):1003537.","journal-title":"PLoS Comput Biol"},{"key":"1077_CR19","unstructured":"Stadler T. Evolving trees: Models for speciation and extinction in phylogenetics. PhD thesis. 2008."},{"issue":"1","key":"1077_CR20","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0025-5564(00)00061-4","volume":"170","author":"M Steel","year":"2001","unstructured":"Steel M, McKenzie A. Properties of phylogenetic trees generated by Yule-type speciation models. Math Biosci. 2001; 170(1):91\u2013112.","journal-title":"Math Biosci"},{"issue":"4","key":"1077_CR21","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1093\/sysbio\/20.4.406","volume":"20","author":"WM Fitch","year":"1971","unstructured":"Fitch WM. Toward defining the course of evolution: Minimum change for a specific tree topology. Syst Biol. 1971; 20(4):406\u201316.","journal-title":"Syst Biol"},{"issue":"4","key":"1077_CR22","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1093\/bioinformatics\/bti191","volume":"21","author":"AP Stamatakis","year":"2005","unstructured":"Stamatakis AP, Ludwig T, Meier H. RAxML-III: A fast program for maximum likelihood-based inference of large phylogenetic trees. Bioinformatics. 2005; 21(4):456\u201363.","journal-title":"Bioinformatics"},{"key":"1077_CR23","doi-asserted-by":"publisher","first-page":"1312","DOI":"10.1093\/bioinformatics\/btu033","volume":"30","author":"Stamatakis A","year":"2014","unstructured":"Stamatakis A. RAxML version 8: A tool for phylogenetic analysis and post-analysis of large phylogenies. Bioinformatics. 2014; 30:1312\u20133.","journal-title":"Bioinformatics"},{"key":"1077_CR24","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198567028.001.0001","volume-title":"Computational molecular evolution","author":"Z Yang","year":"2006","unstructured":"Yang Z, Vol. 284. Computational molecular evolution. New York: Oxford University Press; 2006."},{"key":"1077_CR25","volume-title":"Probability, Markov chains, queues, and simulation: the mathematical basis of performance modeling","author":"WJ Stewart","year":"2009","unstructured":"Stewart WJ. Probability, Markov chains, queues, and simulation: the mathematical basis of performance modeling. Princeton, New Jersey: Princeton University Press; 2009."},{"key":"1077_CR26","volume-title":"7th International School on Formal Methods for Performance Evaluation. LNCS","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska M, Norman G, Parker D. Stochastic model checking In: Bernardo M, Hillston J, editors. 7th International School on Formal Methods for Performance Evaluation. LNCS. Berlin: Springer: 2007. p. 220\u201370."},{"key":"1077_CR27","volume-title":"Model checking","author":"EM Clarke","year":"2000","unstructured":"Clarke EM, Grumberg O, Peled DA. Model checking. Cambridge, Massachusetts: The MIT Press; 2000."},{"issue":"5","key":"1077_CR28","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1016\/j.bbabio.2008.09.003","volume":"1787","author":"J Montoya","year":"2009","unstructured":"Montoya J, L\u00f3pez-Gallardo E, D\u00edez-S\u00e1nchez C, L\u00f3pez-P\u00e9rez MJ, Ruiz-Pesini E. 20 years of human mtDNA pathologic point mutations: Carefully reading the pathogenicity criteria. Biochimica et Biophysica Acta. 2009; 1787(5):476\u201383.","journal-title":"Biochimica et Biophysica Acta"},{"issue":"6","key":"1077_CR29","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/BF01734359","volume":"17","author":"J Felsenstein","year":"1981","unstructured":"Felsenstein J. Evolutionary trees from DNA sequences: A maximum likelihood approach. J Mol Evol. 1981; 17(6):368\u201376.","journal-title":"J Mol Evol"},{"issue":"12","key":"1077_CR30","doi-asserted-by":"crossref","first-page":"1233","DOI":"10.1101\/gr.8.12.1233","volume":"8","author":"P Lio","year":"1998","unstructured":"Lio P, Goldman N. Models of molecular evolution and phylogeny. Genome Res. 1998; 8(12):1233\u201344.","journal-title":"Genome Res"},{"key":"1077_CR31","unstructured":"Cho A. Constructing phylogenetic trees using maximum likelihood. PhD thesis, Scripps Senior These. 2012."},{"key":"1077_CR32","volume-title":"Foundations of phylogenetic systematics","author":"J-W W\u00e4gele","year":"2005","unstructured":"W\u00e4gele J-W. Foundations of phylogenetic systematics. M\u00fcnich: Pfeil; 2005."},{"issue":"3","key":"1077_CR33","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/BF02459467","volume":"59","author":"C Tuffley","year":"1997","unstructured":"Tuffley C, Steel M. Links between maximum likelihood and maximum parsimony under a simple model of site substitution. Bull Math Biol. 1997; 59(3):581\u2013607.","journal-title":"Bull Math Biol"},{"key":"1077_CR34","volume-title":"Proceedings 3rd International Haifa Verification Conference on Hardware and Software, Verification and Testing. LNCS","author":"DN Jansen","year":"2008","unstructured":"Jansen DN, Katoen J-P, Oldenkamp M, Stoelinga M, Zapreev I. How fast and fat is your probabilistic model checker? An experimental performance comparison In: Yorav K, editor. Proceedings 3rd International Haifa Verification Conference on Hardware and Software, Verification and Testing. LNCS. Berlin: Springer: 2008. p. 69\u201385."},{"key":"1077_CR35","volume-title":"Proceedings 23rd International Conference on Computer Aided Verification. LNCS","author":"Marta K","year":"2011","unstructured":"Marta K, Gethin N, David P. PRISM 4.0: Verification of probabilistic real-time systems In: Gopalakrishnan G, Qadeer S, editors. Proceedings 23rd International Conference on Computer Aided Verification. LNCS. Berlin: Springer: 2011. p. 585\u201391."},{"key":"1077_CR36","doi-asserted-by":"publisher","unstructured":"Katoen JP, Khattri M, Zapreev IS. A markov reward model checker. In: Proceedings 2nd International Conference on the Quantitative Evaluation of Systems. IEEE: 2005. p. 243\u2013244, doi:10.1109\/QEST.2005.2.","DOI":"10.1109\/QEST.2005.2"},{"key":"1077_CR37","doi-asserted-by":"crossref","unstructured":"Mateescu R, Requeno JI. On-the-fly model checking for extended action-based probabilistic operators In: Bo\u0161na\u010dki D, Wijs A, editors. 23rd International SPIN Symposium on Model Checking of Software. Springer: 2016. vol. 9641 p. 189\u2013207.","DOI":"10.1007\/978-3-319-32582-8_13"},{"issue":"9","key":"1077_CR38","doi-asserted-by":"publisher","first-page":"975","DOI":"10.1002\/cpe.817","volume":"16","author":"AP Stamatakis","year":"2004","unstructured":"Stamatakis AP, Ludwig T, Meier H. The AxML program family for maximum likelihood-based phylogenetic tree inference. Concurr Comput Pract Experience. 2004; 16(9):975\u201388.","journal-title":"Concurr Comput Pract Experience"},{"issue":"8","key":"1077_CR39","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1038\/nmeth.2109","volume":"9","author":"D Darriba","year":"2012","unstructured":"Darriba D, Taboada GL, Doallo R, Posada D. jModelTest 2: More models, new heuristics and parallel computing. Nat Methods. 2012; 9(8):772\u20132.","journal-title":"Nat Methods"},{"issue":"10","key":"1077_CR40","doi-asserted-by":"publisher","first-page":"1611","DOI":"10.1101\/gr.361602","volume":"12","author":"JE Stajich","year":"2002","unstructured":"Stajich JE, Block D, Boulez K, Brenner SE, Chervitz SA, Dagdigian C, Fuellen G, Gilbert JGR, Korf I, Lapp H, et al. The Bioperl toolkit: Perl modules for the life sciences. Genome Res. 2002; 12(10):1611\u20138.","journal-title":"Genome Res"}],"container-title":["BMC Bioinformatics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s12859-016-1077-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1186\/s12859-016-1077-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s12859-016-1077-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s12859-016-1077-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,1]],"date-time":"2024-02-01T18:07:31Z","timestamp":1706810851000},"score":1,"resource":{"primary":{"URL":"https:\/\/bmcbioinformatics.biomedcentral.com\/articles\/10.1186\/s12859-016-1077-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,14]]},"references-count":40,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2016,12]]}},"alternative-id":["1077"],"URL":"https:\/\/doi.org\/10.1186\/s12859-016-1077-7","relation":{},"ISSN":["1471-2105"],"issn-type":[{"type":"electronic","value":"1471-2105"}],"subject":[],"published":{"date-parts":[[2016,6,14]]},"assertion":[{"value":"19 November 2015","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 May 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 June 2016","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"235"}}