Genetic regulatory networks control the development and functioning of
living organisms. Given that most of the genetic regulatory networks of
biological interest are large and that their dynamics are complex,
understanding their functioning is a major biological problem. Numerous
methods have been developed for the modeling and simulation of such
systems. Surprisingly, the problem of model validation has received little
attention until recently. However, the validation step is very important
since the modeled systems are complex and still imperfectly known.
In this thesis, we propose an approach for testing the validity of models
of genetic regulatory networks by comparing the predictions obtained from
the model with experimental data. We consider a class of qualitative
models of genetic regulatory networks defined in terms of piecewise-linear
(PL) differential equations. While having a simple mathematical form that
favors their symbolic analysis, these models capture essential aspects of
genetic regulation. As experimental information on the dynamics of the
system, we consider the time evolution of the direction of change of
protein concentrations in the network. This information can be
experimentally obtained from temporal expression profiles.
The method that we propose must satisfy two constraints. First, it should
provide predictions that are well-adapted to comparison with the type of
data we consider. Second, it should allow for efficient checks of
consistency between predictions and observations, given the size and the
complexity of the networks of biological interest.
To meet these two constraints, we extend an approach developed by de Jong
and colleagues for symbolic analysis of qualitative PL models in two
directions. First, we propose to use a finer representation of the state
of the system. Through the use of a discrete abstraction, this allows us
to obtain predictions that are better adapted to comparison with
experimental data. Second, we propose to combine this method with
model-checking techniques. We demonstrate that the combined use of
discrete abstraction and model checking makes it possible to check
efficiently dynamical properties, expressed in temporal logic, of
continuous models.
This method has been implemented in a new version of the tool Genetic
Network Analyzer (GNA 6.0). GNA 6.0 has been used for the validation of
two complex models. The first is a model of the initiation of sporulation
in B. subtilis. The second is a model of the nutritional stress
response in E. coli. For both systems, we verify that the
predictions obtained from the models are consistent with most of the
experimental data available in the literature. Several inconsistencies
have also been identified, suggesting either model revisions or the
realization of complementary experiments. In addition to contributing to a
better understanding of the functioning of these systems, these two case
studies illustrate more generally that using the method we propose it is
possible to test whether the predictions obtained from complex models are
consistent with a variety of experimentally-observed properties
