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-transition graphs for more than a century, from state-and-transition models to assembly graphs. Thus, 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. Here we promote the adoption of the model-checking toolbox in ecology through its application to an illustrative example. We assessed the dynamics of a vegetation model inspired from state-and-transition models by model-checking Computation Tree Logic formulas built from a proposed catalogue of patterns. Model-checking encompasses a wide range of concepts and available software, mentioned in discussion, thus its implementation can be fitted to the specific features of the described system. In addition to the automated analysis of ecological state-transition graphs, we believe that defining ecological concepts with temporal logics could help clarifying and comparing 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 despite its successes in systems biology to assess the dynamics of biological networks. We promote model-checking of ecological state-transition graphs through its application to an illustrative vegetation model. We exemplify the insights provided by model-checking by assessing management policies aiming to tackle savanna encroachment. We also provide a catalogue of patterns to help ecologists with the difficulty of formally expressing dynamical properties. We also discuss the wide range of model-checking concepts and available software, enabling to fit the specific features of the studied system, such as durations or probabilities. 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 to the automated analysis of ecological state-transition graphs, we believe that formally defining ecological concepts within the model-checking framework could help in clarifying and comparing them.