Validation de mod�les qualitatifs de r�seaux de r�gulation g�nique : une m�thode bas�e sur des techniques de v�rification formelle

PhD thesis defense, Gr�gory Batt, February 24th 2006, INRIA Rh�ne-Alpes

Abstract in English and full text in French

R�sum� :

Les r�seaux de r�gulation g�nique contr�lent le d�veloppement et le fonctionnement des organismes vivants. Etant donn� que la plupart des r�seaux de r�gulation g�nique d'int�r�t biologique sont grands et que leur dynamique est complexe, la compr�hension de leur fonctionnement est un probl�me biologique majeur. De nombreuses m�thodes ont �t� d�velopp�es pour la mod�lisation et la simulation de ces syst�mes. Etonnamment, le probl�me de la validation de mod�le n'a re�u jusqu'� r�cemment que peu d'attention. Pourtant, cette �tape est d'autant plus importante que dans le contexte de la mod�lisation de r�seaux de r�gulation g�nique, les syst�mes mod�lis�s sont complexes et encore imparfaitement connus.

Dans cette th�se, nous proposons une approche permettant de tester la validit� de mod�les de r�seaux de r�gulation g�nique en comparant les pr�dictions obtenues avec les donn�es exp�rimentales. Plus sp�cifiquement, nous consid�rons dans ce travail une classe de mod�les qualitatifs d�finis en termes d'�quations diff�rentielles lin�aires par morceaux (LPM). Ces mod�les permettent de capturer les aspects essentiels des r�gulations g�niques, tout en ayant une forme math�matique simple qui facilite leur analyse symbolique. Egalement, nous souhaitons utiliser les informations qualitatives sur la dynamique du syst�me donn�es par les changements du sens de variation des concentrations des prot�ines du r�seau. Ces informations peuvent �tre obtenues exp�rimentalement � partir de profils d'expression temporels.

La m�thode propos�e doit satisfaire deux contraintes. Premi�rement, elle doit permettre d'obtenir des pr�dictions bien adapt�es � la comparaison avec le type de donn�es consid�r�. Deuxi�mement, �tant donn� la taille et la complexit� des r�seaux d'int�r�t biologique, la m�thode doit �galement permettre de v�rifier efficacement la coh�rence entre pr�dictions et observations.

Pour r�pondre � ces deux contraintes, nous �tendons dans deux directions une approche pr�c�demment d�velopp�e par H. de Jong et ses coll�gues pour l'analyse symbolique des mod�les LPM qualitatifs. Premi�rement, nous proposons d'utiliser une repr�sentation plus fine de l'�tat du syst�me, permettant d'obtenir, par abstraction discr�te, des pr�dictions mieux adapt�es � la comparaison avec les donn�es exp�rimentales. Deuxi�mement, nous proposons de combiner cette m�thode avec des techniques de model checking. Nous montrons que l'utilisation combin�e d'abstraction discr�te et de model checking permet de v�rifier efficacement les propri�t�s dynamiques, exprim�es en logique temporelle, des mod�les continus.

Cette m�thode a �t� impl�ment�e dans une nouvelle version de l'outil Genetic Network Analyzer (GNA 6.0). GNA 6.0 a �t� utilis� pour la validation de deux mod�les grands et complexes de l'initiation de la sporulation chez B. subtilis et de la r�ponse au stress nutritionnel chez E. coli. Nous avons ainsi pu v�rifier que les pr�dictions obtenues �taient en accord avec la plupart des donn�es exp�rimentales disponibles dans la litt�rature. Plusieurs incoh�rences ont �galement �t� identifi�es, sugg�rant des r�visions des mod�les ou la r�alisation d'exp�riences compl�mentaires. En dehors d'une contribution � une meilleure compr�hension du fonctionnement de ces syst�mes, ces deux �tudes de cas illustrent plus g�n�ralement que, par la m�thode propos�e, il est possible de tester si des pr�dictions obtenues pour des mod�les complexes sont coh�rentes avec un large �ventail de propri�t�s observables exp�rimentalement.