Cargando…

Model-checking ecological state-transition graphs

Model-checking is a methodology developed in computer science to automatically assess the dynamics of discrete systems, by checking if a system modelled as a state-transition graph satisfies a dynamical property written as a temporal logic formula. The dynamics of ecosystems have been drawn as state...

Descripción completa

Detalles Bibliográficos
Autores principales: Thomas, Colin, Cosme, Maximilien, Gaucherel, Cédric, Pommereau, Franck
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Public Library of Science 2022
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC9203009/
https://www.ncbi.nlm.nih.gov/pubmed/35666771
http://dx.doi.org/10.1371/journal.pcbi.1009657
_version_ 1784728639477121024
author Thomas, Colin
Cosme, Maximilien
Gaucherel, Cédric
Pommereau, Franck
author_facet Thomas, Colin
Cosme, Maximilien
Gaucherel, Cédric
Pommereau, Franck
author_sort Thomas, Colin
collection PubMed
description Model-checking is a methodology developed in computer science to automatically assess the dynamics of discrete systems, by checking if a system modelled as a state-transition graph satisfies a dynamical property written as a temporal logic formula. The dynamics of ecosystems have been drawn as state-transition graphs for more than a century, ranging from state-and-transition models to assembly graphs. Model-checking can provide insights into both empirical data and theoretical models, as long as they sum up into state-transition graphs. While model-checking proved to be a valuable tool in systems biology, it remains largely underused in ecology apart from precursory applications. This article proposes to address this situation, through an inventory of existing ecological STGs and an accessible presentation of the model-checking methodology. This overview is illustrated by the application of model-checking to assess the dynamics of a vegetation pathways model. We select management scenarios by model-checking Computation Tree Logic formulas representing management goals and built from a proposed catalogue of patterns. In discussion, we sketch bridges between existing studies in ecology and available model-checking frameworks. In addition to the automated analysis of ecological state-transition graphs, we believe that defining ecological concepts with temporal logics could help clarify and compare them.
format Online
Article
Text
id pubmed-9203009
institution National Center for Biotechnology Information
language English
publishDate 2022
publisher Public Library of Science
record_format MEDLINE/PubMed
spelling pubmed-92030092022-06-17 Model-checking ecological state-transition graphs Thomas, Colin Cosme, Maximilien Gaucherel, Cédric Pommereau, Franck PLoS Comput Biol Research Article Model-checking is a methodology developed in computer science to automatically assess the dynamics of discrete systems, by checking if a system modelled as a state-transition graph satisfies a dynamical property written as a temporal logic formula. The dynamics of ecosystems have been drawn as state-transition graphs for more than a century, ranging from state-and-transition models to assembly graphs. Model-checking can provide insights into both empirical data and theoretical models, as long as they sum up into state-transition graphs. While model-checking proved to be a valuable tool in systems biology, it remains largely underused in ecology apart from precursory applications. This article proposes to address this situation, through an inventory of existing ecological STGs and an accessible presentation of the model-checking methodology. This overview is illustrated by the application of model-checking to assess the dynamics of a vegetation pathways model. We select management scenarios by model-checking Computation Tree Logic formulas representing management goals and built from a proposed catalogue of patterns. In discussion, we sketch bridges between existing studies in ecology and available model-checking frameworks. In addition to the automated analysis of ecological state-transition graphs, we believe that defining ecological concepts with temporal logics could help clarify and compare them. Public Library of Science 2022-06-06 /pmc/articles/PMC9203009/ /pubmed/35666771 http://dx.doi.org/10.1371/journal.pcbi.1009657 Text en © 2022 Thomas et al https://creativecommons.org/licenses/by/4.0/This is an open access article distributed under the terms of the Creative Commons Attribution License (https://creativecommons.org/licenses/by/4.0/) , which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.
spellingShingle Research Article
Thomas, Colin
Cosme, Maximilien
Gaucherel, Cédric
Pommereau, Franck
Model-checking ecological state-transition graphs
title Model-checking ecological state-transition graphs
title_full Model-checking ecological state-transition graphs
title_fullStr Model-checking ecological state-transition graphs
title_full_unstemmed Model-checking ecological state-transition graphs
title_short Model-checking ecological state-transition graphs
title_sort model-checking ecological state-transition graphs
topic Research Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC9203009/
https://www.ncbi.nlm.nih.gov/pubmed/35666771
http://dx.doi.org/10.1371/journal.pcbi.1009657
work_keys_str_mv AT thomascolin modelcheckingecologicalstatetransitiongraphs
AT cosmemaximilien modelcheckingecologicalstatetransitiongraphs
AT gaucherelcedric modelcheckingecologicalstatetransitiongraphs
AT pommereaufranck modelcheckingecologicalstatetransitiongraphs