Grégory Batt (Center for Information and Systems Engineering and Center for BioDynamics, Boston University.)

Natural gene networks are complex networks of interregulating genes that control at the molecular level the development and functioning of living organisms. Synthetic gene networks are engineered networks that confer a desired behavior to a living organism. Understanding the functioning of these networks is a central problem in systems biology and in bioengineering. However, their complex dynamics, due to the presence of feedback loops and non-linear phenomena, often defeats intuitive understanding. Moreover, the lack of precise information on parameter values hampers a model-based analysis or design of these systems.

In this talk, I will present two recently-developed methods for the verification of the dynamical properties of gene networks under parameter uncertainty. Both methods combine discrete abstraction and model checking. Discrete abstraction is used to obtain a discrete representation of the dynamics of the system in the state space for sets of parameters, and model checking is used for the verification of the dynamical properties of the abstract, discrete system. The approximations obtained by discrete abstraction are conservative. This guarantees that the properties satisfied by the abstract system also hold for the original one.

The above strategy is applied to the analysis of two different types of models, namely piecewise affine and piecewise multiaffine differential equation models. Both types of models capture essential features of genetic regulations but with different levels of detail. A coarse-grained, qualitative approach is used for the analysis of piecewise affine models. This method is well-adapted to the essentially qualitative information available on natural gene networks. A finer-grained, quantitative approach is used for the analysis of piecewise multiaffine models, well-adapted to the better-known synthetic gene networks. Though quantitative, this approach can deal with uncertain parameters specified by intervals.
The practical applicability and biological relevance of the proposed approaches are illustrated by means of two examples: the validation of a model of the nutritional stress response and the tuning of a synthetic transcriptional cascade, both in the bacterium E. coli.

Work done in collaboration with: - Hidde de Jong (INRIA), Johannes Geiselmann (UJF, Grenoble), Jean-Luc Gouzé (INRIA), Radu Mateescu (INRIA), Michel Page (UPMF, Grenoble), Delphine Ropers (INRIA), Tewfik Sari (UHA, Mulhouse) and Dominique Schneider (UJF, Grenoble) and - Calin Belta (Boston University), Boyan Yordanov (Boston University) and Ron Weiss (Princeton University)