CTL (Computation Tree Logic)

Introduction

Computation Tree Logic (CTL) is one of the most popular temporal logics because it is particularly fitted to express properties of branching dynamics with alternative pathways. ecco is using CTL because ecological systems often involves alternative pathways. A CTL formula describes a property over computation trees, noted CTs as in the beginning of CTL. A CT is rooted at a given state of the state-space, and its branches are the alternative pathways starting from this state. In computer science, a state-space usually represents the behaviors of a software system, thus every branch of a CT represents an alternative software computation, hence the name ‘’computation tree’‘.

For instance, we can consider two dynamics of the Borona region in Ethiopia: (a) before livestock introduction, fire was used to burn trees and/or bushes; (b) after livestock introduction, using fire has been banned by the government, and bushes tend to grow until the land is fully encroached.

These two state-spaces have a state ‘’open canopy woodland’’ that can be considered as the root of a computation tree. This yields two possible CTs:

Each branch descending from the root state ‘’open canopy woodland’’ represents a possible pathway in the corresponding dynamics. (a) As the pathways are infinite in this dynamics, the branches of the CT are also infinite, and thus the CT itself. (b) The grassland state is not reachable from the open canopy woodland state in this dynamics, and thus it does not appear in its CT. As the pathways are finite in this dynamics, the branches of the CT are also finite, and thus the CT itself.

Here are two examples of CTL dynamical properties to foster intuition:

• all the CT’s pathways eventually lead to an encroached state
• at least one of the CT’s pathways maintains grasses

A CTL model-checker checks whether the CT rooted in each state satisfies a CTL formula or not. Thus, a CTL model-checker discriminates between the states whose CT satisfies a given property and those whose CT does not.

Syntax and interpretation

The syntax of CTL is as follows:

A state property \(p\) is a Boolean property mapping over states. In ecco, the concrete syntax for state properties depends on the modelling language that is used, for instance with RR, state properties may be A+ (or equivalently just A) or A-, where A is a variable.

More complex formulas are built by combining sub-formulas using the Boolean logical operators: not (\(\lnot\)), and (\(\land\)), or (\(\lor\)). In ecco, since these symbols are not available on keyboards, we use the Python operators ~, &, and | instead. Similarly, we use True instead of \(\top\). Other Boolean logical operators can be built on top of the three ones above, such as the implication (\(\Rightarrow\), or => in ecco) that is defined such that \(p \Rightarrow q\) is equivalent to \((\lnot p) \lor q\). Since CTL properties are interpreted as sets of states (whose CTs validate the property), Boolean operations can be interpreted as sets operations: \(\lnot\) is complement, \(\land\) is intersection, and \(\lor\) is union.

The temporal operators of CTL are always the combination of two types of operators:

• first a quantifier (\(\mathrm{E}\) or \(\mathrm{A}\)) dealing with branching by quantifying over the pathways starting from a given state
• second a modality (\(\mathrm{F}\), \(\mathrm{G}\), or \(\mathrm{U}\)) specifying the order of properties along a pathway

Temporal operators can thus be separated between existential and universal operators. Existential operators (\(\mathrm{EF}\), \(\mathrm{EG}\), or \(\mathrm{EU}\)) specify that their modality has to be verified by at least one branch of the CT (thus by at least one pathway starting from its root state). Universal operators (\(\mathrm{AF}\), \(\mathrm{AG}\), or \(\mathrm{AU}\)) specify that their modality has to be verified by every branch of the CT (thus by every pathway starting from its root state). Modality \(\mathrm{F}\) specifies that the property finally becomes true at one step of the pathway. Modality \(\mathrm{G}\) specifies that the property is globally true all along the pathway. Modality \(\mathrm{U}\) specifies that the left-hand-side property remains true along the pathway until the right-hand-side property finally becomes true. (CTL also defines modality next \(\mathrm{X}\), but we omit it to simplify the presentation.) This is illustrated in this picture:

existential examples	universal examples
\(\mathrm{EF}\) black	\(\mathrm{AF}\) black
\(\mathrm{EG}\) black	\(\mathrm{AG}\) black
\(\mathrm{E}(\)grey \(\mathrm{U}\) black\()\)	\(\mathrm{A}(\)grey \(\mathrm{U}\) black\()\)

For example, in the CTs from the Borona model shown above, where variable Tr is on in the states where a tree is drawn:

• the CTL formula EF Tr- specifies that a state without trees is reachable from the root of the CT, which is satisfied in CT (a) but not in CT (b)
• the CTL formula EG Tr+ specifies that trees are always present along at least one branch of the CT, which is satisfied for the left-most branch in CT (a) but not for its other branches, thus this CTL property is satisfied in both CT (a) and CT (b)
• the CTL formula AG Tr+ specifies that trees are always present all along every branch of the CT, which is satisfied in CT (b), but not in CT (a)

Lastly, CTL operators can be nested to express even subtler temporal behavior. For example, AG(EF Tr-) specifies that: all along every pathway (AG), the pathway can always branch off to reach a future state (EF) without trees (Tr-). While AG(EF Tr-) holds in CT (a), the simpler property AF Tr- does not because trees never disappear in the left-most branch of the CT.

Building formulas from patterns

Translating a dynamical property (i.e. a description of an ecosystem behavior) written in English into a CTL formula can turn out to be a delicate exercise for non-expert users. One possible way to simplify this task is to provide users with a catalog mapping query patterns to their translations in CTL. In the patterns below, \(x\) and \(y\) are place-holders for other properties.

This patterns can be nested to build arbitrarily complex formulas, but whose meaning may be complex to grasp intuitively. The TL wizard is an interactive formula editor based on these patterns, it allows building formulas in an easy and structured way.