Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation

Résumé Technique : Accessibilité dans les systèmes dynamiques biochimiques par approximation discrète quantitative

Énoncé du problème
La biologie des systèmes vise à reconstruire des modèles exécutables d'organismes vivants pour étudier les comportements émergents issus de la biochimie sous-jacente. Bien que les équations différentielles ordinaires (EDO) soient la norme pour modéliser ces systèmes dynamiques biochimiques, elles présentent des défis importants pour l'analyse globale. Plus précisément, le problème de l'accessibilité (reachability) — déterminer si un phénomène dynamique (par exemple, une oscillation ou des niveaux de concentration spécifiques) se produit pour toutes les conditions initiales considérées — est généralement indécidable en raison de la nature non bornée et non dénombrable des espaces d'états continus.

Les méthodes d'analyse existantes reposent souvent sur la simulation numérique, qui est limitée à une analyse « locale » partant d'un seul point initial. Pour parvenir à une analyse globale, les chercheurs utilisent des approximations discrètes finies, telles que les abstractions rectangulaires. Cependant, les techniques traditionnelles d'abstraction rectangulaire souffrent de niveaux élevés de « comportements fallacieux » (spurious behavior). Car ces méthodes sur-approximent le champ de vecteurs sur les frontières entre les rectangles (facettes) sans suivre l'historique spécifique des trajectoires, générant ainsi de nombreuses séquences d'états qui ne correspondent à aucune trajectoire réelle dans le système continu. Augmenter la densité de la partition n'élimine pas toujours ce problème de manière efficace.

Méthodologie
Les auteurs proposent une nouvelle technique de calcul pour l'approximation discrète finie de systèmes dynamiques continus, ciblant spécifiquement les systèmes biochimiques modélisés par des champs de vecteurs multi-affines (affines dans chaque variable). Le cœur de la méthode est l'Automate d'Approximation Discrète Quantitative (QDAA).

1. Définition de l'état : Contrairement aux abstractions rectangulaires standards où un état est simplement un rectangle, un état dans le QDAA est défini comme une paire $\langle H, E \rangle$, où $H$ est un rectangle (une cellule dans l'espace d'état partitionné) et $E$ est un « ensemble d'entrée » (entry set). L'ensemble d'entrée $E$ représente un sous-ensemble d'une facette spécifique de $H$ par laquelle les trajectoires entrent dans le rectangle. Cette mémoire locale encode l'évolution de l'historique du système.
2. Quantification via les sous-ensembles focaux : Pour chaque état $\langle H, E \rangle$, la méthode identifie des « sous-ensembles focaux ». Ce sont des sous-ensembles de l'ensemble d'entrée à partir desquels toutes les trajectoires évoluent vers une facette de sortie spécifique (ou restent dans le rectangle indéfiniment).
3. Transitions pondérées : Les transitions entre les états sont assignées des poids basés sur le volume relatif (mesure de Lebesgue) de ces sous-ensembles focaux. Plus précisément, le poids d'une transition d'un état $A$ vers un état $B$ correspond au volume de la partie de l'ensemble d'entrée de $A$ qui mène à $B$, divisé par le volume total de l'ensemble d'entrée de $A$. Cela transforme le QDAA en une chaîne de Markov à temps discret.
4. Discrétisation et approximation : Pour rendre le calcul réalisable, les volumes continus sont approximés en discrétisant les facettes en une grille uniforme de $\kappa$-tuiles. Des simulations numériques sont employées pour identifier les régions d'entrée et les sous-ensembles focaux. Le paramètre $\kappa$ contrôle la granularité de la discrétisation.
5. Convergence : La méthode est conçue de telle sorte qu'à mesure que le paramètre de discrétisation $\kappa$ augmente, la mesure de volume approximative converge vers la mesure de volume continue, réduisant ainsi l'écart entre le comportement continu original et son approximation.

Principales contributions
Le document présente quatre contributions primaires :

1. Une nouvelle technique de calcul : L'introduction du QDAA pour l'approximation discrète finie de systèmes dynamiques multi-affines. Cette technique augmente l'abstraction rectangulaire standard avec une mémoire locale (ensembles d'entrée) et des poids quantitatifs.
2. Preuve de convergence : Une démonstration théorique (Théorème 3.3) que le QDAA converge vers le comportement du système continu original lorsque le paramètre de discrétisation $\kappa$ tend vers l'infini.
3. Algorithme d'accessibilité : Le développement d'algorithmes spécifiques (Algorithmes 1 et 2) pour calculer l'espace d'états accessible du QDAA. Ces algorithmes utilisent une recherche en largeur et des simulations numériques (incluant des simulations en arrière pour affiner les ensembles d'entrée) afin de déterminer les successeurs et les poids de transition.
4. Évaluation empirique : L'application et l'évaluation de la méthode sur plusieurs modèles biologiques, incluant une variante oscillatoire de Lotka-Volterra, un modèle de cinétique enzymatique et une étude de cas réelle de l'assimilation de l'ammonium chez E. coli.

Résultats
Les auteurs ont évalué la méthode sur des modèles de dimensions deux, quatre et sept.

• Modèles oscillatoires et enzymatiques : Les résultats ont démontré qu'augmenter $\kappa$ améliore la précision de l'analyse d'accessibilité. Pour le modèle oscillatoire, le QDAA a fourni une représentation plus précise des états accessibles par rapport à l'abstraction rectangulaire standard, qui sur-approximait l'espace accessible à l'ensemble de l'espace des phases.
• Étude de cas E. coli : Dans le modèle de transport de l'ammonium, les résultats du QDAA pour la concentration d'ammonium intracellulaire ($NH_4in$) étaient nettement plus proches des données de simulation numérique que ceux obtenus via l'abstraction rectangulaire standard. Les résultats du QDAA étaient à moins d'un ordre de grandeur de la simulation, alors que l'abstraction rectangulaire sur-approximait les limites de manière significative.
• Comportement fallacieux : L'évaluation a confirmé que le QDAA réduit efficacement l'étendue du comportement fallacieux (faux positifs en accessibilité) inhérent aux abstractions rectangulaires conservatrices.

Signification et affirmations
L'article affirme que la méthode proposée offre un changement pratique dans l'application des méthodes formelles aux systèmes complexes. En combinant la simulation numérique avec l'abstraction rectangulaire, le QDAA évite les extrêmes d'être purement une sur-approximation ou une sous-approximation. Au lieu de cela, il fournit une approximation paramétrée où le niveau de précision peut être ajusté.

Les auteurs affirment que la méthode est suffisante pour approximer l'accessibilité dans des systèmes dynamiques biochimiques complexes. Elle sert deux rôles potentiels :

1. Comme une technique de simulation paramétrée pour obtenir des vues globales de la dynamique.
2. Comme un outil pour quantifier et éliminer les contre-exemples fallacieux lorsqu'elle est utilisée conjointement avec l'abstraction rectangulaire pour le model checking.

Le travail est présenté comme une version complète d'un article de conférence, offrant une fondation théorique et un prototype d'implémentation (en C++) qui démontre des résultats satisfaisants pour le calcul de l'accessibilité dans des modèles biologiques de faible à moyenne dimension. Les auteurs notent que les travaux futurs incluent l'intégration de la méthode dans les logiciels de model checking existants et le développement d'algorithmes parallèles pour gérer les systèmes de dimension supérieure.