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.

A state-and-transition model to guide grassland management

Grassland ecosystems across the globe have been extensively modified and degraded by agriculture and urban development, leaving conservation managers with a complex set of interacting legacies and opportunities to contend with. We advocate the use of state-and-transition models to assist conservation managers to deal with this complexity. Using a major development and compensation project as a case study (The Melbourne Strategic Assessment under the Australian Environment Protection and Biodiversity Conservation Act 1999), we discuss the uses and limitations of state-and-transition models for conservation management. We define a state-and-transition model for an endangered Australian temperate grassland. Soil and vegetation data are used to evaluate the model and confirm that the assigned states relate to observable agro-ecological patterns. We then discuss the use of this model for several different interacting purposes: as a tool for the simple communication of complex ecological processes; as a tool for landscape stratification to aid the spatial application of management and experimentation; as a framework to set and define conservation objectives; and as an aide for adaptive management.