TITLE :

Logics for discrete gene regulatory networks
(Gilles Bernot)

ABSTRACT :

The beginning of the course presents the basic modelling approach defined by
René Thomas (Brussels) in the 70's. We firstly explain how the space of
possible gene expression levels can be decomposed into several intervals in
order to obtain a discrete qualitative description of gene networks. Then, we
show how this discrete approach can be formalized and how the minimal set of
Thomas' parameters is used to build an "asynchronous" automaton from the gene
interaction graph. This automaton models the dynamic behaviour of the
regulatory network (chronological evolution of the gene expression levels).

The main difficulty when modelling gene networks is the identification of the
parameters that govern the dynamics. We show how to use temporal logic in
order to extract unknown parameter values from the observed behaviours. We
firstly give an overview on CTL (Computation Tree Logic) and its associated
model checking methods. We show how it can be used in order to find the set of
possible parameter values, i.e., parameters that are consistent with the known
qualitative behaviours. Some complementary reasonings, taking into account the
biological question under interest, can also help reducing the size of the
gene network model.

We also present a new approach based on Hoare logic and an associated weakest
precondition calculus that generates constraints on the parameter values. Once
proper specifications are extracted from biological traces (e.g. based on
transcriptomic data), they play a role similar to programs in the classical
Hoare logic. The method is correct and complete w.r.t. the Thomas' semantics.

Lastly, we sketch how some logical considerations can be used in order to
generate interesting "wet" biological experiments, starting from the formal
descriptions of the interaction graph and the biological hypotheses under
consideration.

A few biological examples of small size will illustrate the notions defined
during the course.