Sub-Saharan social-ecological systems are undergoing changes in environmental conditions, including modifications in rainfall pattern and biodiversity loss. Consequences of such changes depend on complex causal chains which call for integrated management strategies whose efficiency could benefit from ecosystem dynamic modeling. However, ecosystem models often require lots of quantitative information for estimating parameters, which is often unavailable. Alternatively, qualitative modeling frameworks have proved useful for explaining ecosystem responses to perturbations, while only requiring qualitative information about social-ecological interactions and events and providing more general predictions due to their validity for wide ranges of parameter values. In this paper, we propose the Ecological Discrete-Event Network (EDEN), an innovative qualitative dynamic modeling framework based on “if-then” rules generating non-deterministic dynamics. Based on expert knowledge, observations, and literature, we use EDEN to assess the effect of permanent changes in surface water and herbivores diversity on vegetation and socio-economic transitions in an East African savanna. Results show that water availability drives changes in vegetation and socio-economic transitions, while herbivore functional groups have highly contrasted effects depending on the group. This first use of EDEN in a savanna context is promising for bridging expert knowledge and ecosystem modeling.

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.

Acting systems aim at refining high-level actions into executable commands, while managing access to resources, possible failures, or any other unpredictable situation. Improving the trust on autonomous robots also requires to have a formal model of acting, and the capability to perform some analysis on this model. In this paper, we present ASPiC, an acting system based on the modeling of robot's skills using a specific control-flow Petri net model. The skills can then be combined using well-defined operators to build a complete plan that refines a high-level action. Some properties are guaranteed by construction, while others can be verified on the resulting plan model. ASPiC is finally applied to an area protection mission by an autonomous surface vehicle.

Trophic interaction networks are notoriously difficult to understand and to diagnose (i.e., to identify contrasted network functioning regimes). Such ecological networks have many direct and indirect connections between species, and these connections are not static but often vary over time. These topological changes, as opposed to a dynamic on a static (frozen) network, can be triggered by natural forcings (e.g., seasons) and/or by human influences (e.g., nutrient or pollution inputs). Aquatic trophic networks are especially dynamic and versatile, thus suggesting new approaches for identifying network structures and functioning in a comprehensive manner. In this study, a qualitative model was devised for this purpose. Applying discrete-event models from theoretical computer science, a mechanistic and qualitative model was developed that allowed computation of the exhaustive dynamics of a given trophic network and its environment. Once the model definition is assumed, it provides all possible trajectories of the network from a chosen initial state. In a rigorous and analytical approach, for the first time, we validated the model on one theoretical and two observed trajectories recorded at freshwater stations in the La Rochelle region (Western France). The model appears to be easy to build and intuitive, and it provides additional relevant trajectories to the expert community. We hope this formal approach will open a new avenue in identifying and predicting trophic (and non-trophic) ecological networks.