부산대학교 도서관

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. Author summary: Ecologists have drawn state-transition graphs representing the dynamics of ecosystems for more than a century. Model-checking is an automated method for the analysis of such graphs developed in computer science and acknowledged by a Turing award in 2007. Ecologists appear to be mostly unaware of model-checking apart from precursory applications, despite its successes in systems biology. We propose to address this situation, through an inventory of existing ecological state-transition graphs and an accessible presentation of the model-checking methodology. We exemplify the insights provided by model-checking by applying it to a vegetation pathways model in order to assess management policies aiming to tackle savanna encroachment. We provide a catalogue of patterns to help ecologists with the difficulty of formally expressing dynamical properties. Lastly, we sketch bridges between existing studies in ecology and available model-checking frameworks. Model-checking can be applied to both empirical data and theoretical models, as long as they sum up into state-transition graphs. It provides automated and accurate answers to complex questions that could barely be analysed through human examination, if not impossible to answer this way. In addition, we believe that formally defining ecological concepts within the model-checking framework could help clarify and compare them. [ABSTRACT FROM AUTHOR]