Note publique d'information : Les réseaux de régulation biologiques (RRB) représentent les interactions entre des
entités biologiques. Par exemple, les réseaux de régulation génétiques sont des graphes
dont les sommets représentent les gènes ou les produits (ARN ou protéines) et les
arcs représentent leurs interactions. Cette thèse propose le formalisme d'automates
hybride linéaire (AHL) pour l'analyse automatique des dynamiques des RRB. Le formalisme
qualitatif de René Thomas est une approche bien connue pour la modélisation discrète
et l'analyse des dynamiques des RRB. Il détermine le comportement qualitatif des RRB
d'une manière rigoureuse. A partir d'un modèle discret, il n'est pas réellement possible
(à cause de l'abstraction complète du temps) de déterminer des trajectoires particulières
et en particulier des trajectoires cycliques ou non-cycliques. En nous basant sur
le formalisme discret de René Thomas, nous introduisons la modélisation hybride des
RRB par le formalisme des automates hybrides linéaires (AHL) qui prennent en compte
les délais de production et de dégradation des produits de gènes. La modélisation
hybride capture les deux types de comportement c'est-à-dire l'évolution discrète de
niveau d'expression ainsi que l'aspect temporel (avec le temps) d'évolution continue
des produits de gènes. Cette modélisation nous permet de faire l'analyse des AHL par
l'outil de model-checking comme Hy-Tech pour l'accessibilité, les comportements cycliques
comme le noyau d'invariance, les états stables et les chemins entre deux états donnés.
Ces comportements abordent les aspects qui sont intéressants pour les biologistes.
Par exemple, les cycles représentent l'homéostasie tandis que les états stables représentent
la multi-stationnarité. Tous les comportements que nous analysons sont caractérisés
par des contraintes de délais. Ces contraintes sont des conditions pour l'existence
de ces différents comportements. Nous présentons les méthodes pour les calculs de
la longueur, du volume et du diamètre du noyau d'invariance. Ces différentes mesures
nous permettent d'introduire une notion de stabilité du noyau d'invariance. L'approche
de modélisation hybride est appliquée sur plusieurs exemples réels des RRB. Ces exemples
sont le RRB de la bactérie Pseudomonas aeruginosa, le RRB du cycle circadien du mammifère,
le RRB du virus phage lambda, le système d'activation et de latence de la cellule-T
et le réseau pour la réponse de la carence en carbone chez Escherichia coli.
Note publique d'information : Biological regulatory networks (BRN) represent interactions among the biological entities.
For example, genetic regulatory networks are graphs where vertices stand for genes
or their products (RNA or proteins) and edges represent interactions among them. The
aim of this thesis is to propose a hybrid modelling formalism in order to automatically
analyse the dynamics of the BRN. The qualitative formalism of René Thomas is a well-known
approach for the discrete modelling of BRN. Due to the complete abstraction of time
in the formalism of René Thomas, it is not possible to distinguish between cyclic
and non-cyclic behaviours of BRN. Based on the discrete formalism of René Thomas,
we introduce the hybrid modelling of BRN by using the formalism of linear hybrid automata
(LHA) that takes into account the production and degradation delays of genes' products.
The hybrid modelling captures both the discrete evolution of genes' expressions and
the temporal aspect (with time) of the continuous evolution of genes' products. The
hybrid modelling allows us to automatically analyse a BRN by a model-checking tool,
for example HyTech, for cyclic behaviour (the so-called invariance kernel), stable
states and paths between two given states. These behaviours have biological signicances.
For example, cycles represent homeostasy while stable states represent multistationarity.
These behaviours are characterised by the delay constraints, which are considered
as necessary and sucient conditions for the existence of these behaviours. We present
a method for the computation of length, volume and diameter of the invariance kernel.
These dierent measuring features allow us to introduce the notion of stability of
the invariance kernel. The hybrid modelling formalism is applied on some biological
examples. These examples are the BRN of the bacterium pseudomonas aeruginosa, the
BRN of the circadian cycle of mammals, the BRN of the virus lambda phage, the activation
and anergy system of the T-cell and the carbon starvation response network of the
Escherichia coli.