une extension de la logique de Hoare pour les réseaux génétiques

Gilles Bernot, Jean-Paul Comet et Zohra Khalis

Résumé:

L'étape la plus délicate de la modélisation des réseaux de régulation génétique est l'identification des paramètres des modèles menant à des dynamiques compatibles avec les connaissances sur le système biologique. Ainsi, on cherche souvent exhaustivement l'ensemble des valeurs des paramètres qui sont cohérents avec la formalisation des observations expérimentales. L'utilisation des contraintes est alors utile pour représenter d'une manière algébrique l'ensemble des paramétrages d'intérêt. Dans cet exposé, nous nous focaliserons sur la modélisation qualitative de R. Thomas et nous présenterons une nouvelle approche pour générer des contraintes sur les valeurs possibles des paramètres. Cette approche est basée sur une extension de la logique de Hoare. Nous introduisons à cette occasion une nouvelle formalisation de la dynamique asynchrone classique. Une des caractéristiques de cette nouvelle approche réside dans le fait que la spécification du système est donnée par les comportements possibles exprimés sous forme d'ensemble de chemins, qui sont décrits par un "programme". Enfin puisque cette méthode ne nécessite pas la construction du graphe d'états complet, elle constitue un outil très puissant pour trouver les valeurs des paramètres; en particulier, on gère très facilement des knock-out / reprises d'activité imposés au cours des protocoles expérimentaux.

Travail présenté au colloque "Formalisme logique, apports et défis pour la modélisation de réseaux de régulation biologique", Rabat, Maroc, 12-15 avril 2011.