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.