TITLE :

Formal approaches to model gene regulatory networks
(Gilles Bernot)

ABSTRACT :

The first part of the course will develop the basic modelling approach
introduced by René Thomas (Brussels) in the 70's. We will 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. We will then show how this discrete approach can be
formalized (according to formal methods of computer science). The
parameters of the Thomas'approach are used in order to build
an "asynchronous" automaton from the gene interaction graph. This
automaton mathematically models the dynamic behaviour of the regulatory
network (time evolution of the expression levels).

The second part of the course will focus on current research works. We will
show how to use formal logic in order to extract unknown parameter values from
the observed behaviours. We will firstly give a short course on formal
temporal logics and their associated model checking methods. We will then show
how model checking can be used in order to find the set of possible parameter
values, i.e. parameters which are consistent with the known qualitative
behaviours. Complementary results can be used in order to reduce the size of
this set of consistent parameters: we shall explain how to use the notion of
"functionality" of a path in the interaction graph. Lastly, we will explain
how some of the current software testing methods can be used in order to
generate interesting "wet biology" experiments, starting from the formal
descriptions of the interaction graph and the biological hypotheses under
consideration.

Some examples will be used to illustrate the notions defined during the
course. In particular the simple model of mucus production in Pseudomonas
aeruginosa will be fully studied. Pseudomonas aeruginosa is a opportunistic
bacteria which infects the lungs of patients of cystic fibrosis.