"Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis

Abstract

Background: In Thomas' formalism for modeling gene regulatory networks (GRNs), branching time, where a state can have more than one possible future, plays a prominent role. By representing a certain degree of unpredictability, branching time can model several important phenomena, such as (a) asynchrony, (b) incompletely specified behavior, and (c) interaction with the environment. Introducing more than one possible future for a state, however, creates a difficulty for ordinary simulators, because infinitely many paths may appear, limiting ordinary simulators to statistical conclusions. Model checkers for branching time, by contrast, are able to prove properties in the presence of infinitely many paths.

Results: We have developed Antelope ("Analysis of Networks through TEmporal-LOgic sPEcifications", http://turing.iimas.unam.mx:8080/AntelopeWEB/), a model checker for analyzing and constructing Boolean GRNs. Currently, software systems for Boolean GRNs use branching time almost exclusively for asynchrony. Antelope, by contrast, also uses branching time for incompletely specified behavior and environment interaction. We show the usefulness of modeling these two phenomena in the development of a Boolean GRN of the Arabidopsis thaliana root stem cell niche.There are two obstacles to a direct approach when applying model checking to Boolean GRN analysis. First, ordinary model checkers normally only verify whether or not a given set of model states has a given property. In comparison, a model checker for Boolean GRNs is preferable if it reports the set of states having a desired property. Second, for efficiency, the expressiveness of many model checkers is limited, resulting in the inability to express some interesting properties of Boolean GRNs.Antelope tries to overcome these two drawbacks: Apart from reporting the set of all states having a given property, our model checker can express, at the expense of efficiency, some properties that ordinary model checkers (e.g., NuSMV) cannot. This additional expressiveness is achieved by employing a logic extending the standard Computation-Tree Logic (CTL) with hybrid-logic operators.

Conclusions: We illustrate the advantages of Antelope when (a) modeling incomplete networks and environment interaction, (b) exhibiting the set of all states having a given property, and (c) representing Boolean GRN properties with hybrid CTL.

Figure 1

A fragment of the state-transition graph of a Boolean GRN exemplifying asynchrony. Assume that the behavior of a network specifies a simultaneous transition of the value of the two rightmost genes from 0 to 1 (panel (a)). If we exclude the possibility of simultaneous changes, it might be more realistic to model such a phenomenon with an indetermination (panel (b)).

Figure 2

A fragment of the state-transition graph of a Boolean GRN showing the appearance of infinitely many paths. Infinitely many paths appear in this Boolean GRN because of one state (s₁) having more than one future and occurring in a cycle. Some paths are: (s₀s₁s₂ ...), (s₀s₁s₁s₂ ...), (s₀s₁s₁s₁s₂ ...), ... A simulator using a random device traverses the model forward, state by state, following a single path of the state graph, limiting the use of such a tool to drawing only statistical conclusions about all paths in models such as this one. Model checkers, by contrast, can prove precise properties, even in the presence of infinitely many paths resulting from states having more than one future.

Figure 3

The interaction diagram of the GRN underlying cell type determination in the root stem cell niche of the model plant A. thaliana. The abbreviated names of the genes are inside ellipses and the edges correspond to the regulatory interactions. Auxin is a morphogene. The genes are: Auxin/INDOLE-3-ACETIC ACID (Aux/IAA), AUXIN RESPONSE FACTOR (ARF), JACKDAW (JKD), MAGPIE (MGP), PLETHORA (PLT), SCARECROW (SCR), SHORTROOT (SHR), and WUSCHEL-RELATED HOMEBOX5 (WOX5). Ordinary arrow heads denote activation; T-bar arrow heads denote inhibition.

Figure 4

Screenshot of Antelope showing the stable steady states for the stem cell niche GRN without indeterminations. The upper frame displays the name of the file being analyzed, the analysis performed (with the Hybrid CTL formula), and the mode by which the property was checked (synchronous or asynchronous). The middle frame displays the analysis results. The bottom frame displays new actions that can be done. The stable steady states correspond to the root SCN cellular types.

Figure 5

Screenshot of Antelope showing the results for unstable steady state search for the stem cell niche GRN with an indetermination in the SCR logical rule. This indetermination represents a mutation in FAS. As observed, SCR activity is present even in the absence of SHR, which is indispensable for SCR activity. It is important to note that some of the changes can only be observed analyzing the basins of attraction. For instance, the steady states for QC and CEI (two different cell types) are not possible without SCR presence; hence, a change of one steady state for another is only observable through their basins of attraction.