The Ph.D. defense was on February 24th, 2006 at INRIA Rhone-Alpes.
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.
Validation of qualitative models of genetic regulatory networks: a method based on formal verification techniques |
