A Timed Modelling Framework for Gene Regulatory Networks Analysis

Fig. 1: A sigmoid curve (a), its logical caricature (b), and its piecewise linear caricature (c)

Our aim is to account for these time delays (one delay for increasing and one for decreasing). For this purpose, we designed a more accurate abstraction of GRN where delays are now supposed to be non null unknown parameters. In the new designed modelling framework, we add clock variables (one clock for each gene) which measure times of increase or decrease, the dynamics of which are either -1, 0 or +1. Thus, the behaviour of the system Is such that we stay in one location until a deadline is reached (i.e. the clock of one gene is equal to one of the linked delays).
The final model is obtained when we put together all the locations according to the relevant relations of discrete transitions. Each discrete transition is compound of a guard (condition of firing), an action (which takes place when the transition is fired, and the new location to go. In each location, continuous transitions take place according to some dynamics such that dhx/dt is in {-1, 0, +1}. This makes up a hybrid automata.

Fig. 2: The model for one location when x-expression level is 1 and y's is 0. (arrows show the different behaviours from one state in the location)

We show that we can apply parameterized hybrid model-checking algorithms on these models, in order to analyse the behaviour of a network of interacting genes. Our current specific interests are mainly about the characteristics of the cyclic versus divergent trajectories in the possible executions of the model, in order to compare with the observed actual behaviour.

BioAtlanStic:

The text of the project (in french) [repAtlanStic.pdf]

BIL:

The text of the project (in french) [bil.pdf]

REGULATHON: