RESUMO
Ecosystem modeling is a complex and multidisciplinary modeling problem which emerged in the 1950s. It takes advantage of the computational turn in sciences to better understand anthropogenic impacts and improve ecosystem management. For that purpose, ecosystem simulation models based on difference or differential equations were built. These models were relevant for studying dynamical phenomena and still are. However, they face important limitations in data-poor situations. As a response, several formal and non-formal qualitative dynamical modeling approaches were independently developed to overcome some limitations of the existing methods. Qualitative approaches allow studying qualitative dynamics as relevant abstractions of those provided by quantitative models (e.g., response to press perturbations). Each modeling framework can be viewed as a different assemblage of properties (e.g., determinism, stochasticity or synchronous update of variable values) designed to satisfy some scientific objectives. Based on four stated objectives commonly found in complex environmental sciences ((1) grasping qualitative dynamics, (2) making as few assumptions as possible about parameter values, (3) being explanatory and (4) being predictive), our objectives were guided by the wish to model complex and multidisciplinary issues commonly found in ecosystem modeling. We then discussed the relevance of existing modeling approaches and proposed the ecological discrete-event networks (EDEN) modeling framework for this purpose. The EDEN models propose a qualitative, discrete-event, partially synchronous and possibilistic view of ecosystem dynamics. We discussed each of these properties through ecological examples and existing analysis techniques for such models and showed how relevant they are for environmental science studies.
RESUMO
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.