Abstractions de différences exactes de réseaux de réactions : améliorer la précision de prédiction de changements de systèmes biologiques

Des prédictions de changements pour des réseaux de réactions avec information cinétique partielle peuvent être obtenues par raisonnement qualitatif avec l'interprétation abstraite. Un problème de prédiction classique en biologie systémique est de savoir quels knock-outs de gènes peuvent, ou doivent, augmenter le flux de sortie d'une espèce ciblée à l'état stationnaire. Répondre à une telle question pour un réseau de réactions donné demande de raisonner avec des différences abstraites telles que "augmenter'' et "diminuer''. Une tâche fondamentale pour des prédictions de changements a été présenté par Niehren, Versari, John, Coutte, et Jacques (2016). Il s'agit du problème de calcul de l'abstraction de différences d'un ensemble de solutions positives d'un système d'équations linéaires avec des contraintes de différences non linéaires.Précédemment, des algorithmes de surapproximation pour cette tâche ont été proposé en utilisant différentes heuristiques, par exemple basées sur la réécriture des équations linéaires. Dans cette thèse, nous présentons les premiers algorithmes exacts pouvant résoudre cette tâche pour les deux abstractions de différences utilisées dans la littérature.En guise de première contribution, nous montrons pour un système d'équations linéaires, comment caractériser l'abstraction booléenne de l'ensemble de ces solutions positives. Cette abstraction associe 1 à n'importe quel réel strictement positif, et 0 à 0. La caractérisation est donnée par l'ensemble des solutions booléennes d'un autre système d'équations, qui est obtenu à partir des modes élémentaires. Les solutions booléennes de ce système caractéristique peuvent être calculées en pratique à l'aide de la programmation par contraintes sur les domaines finis. Nous pensons que ce résultat est intéressant pour l'analyse de programmes fonctionnels avec arithmétiques linéaires.Comme seconde contribution, nous présentons deux algorithmes qui calculent, pour un système d'équations linéaires et de contraintes à différences non linéaires donné, l'abstraction de différences en Delta_3 et respectivement en Delta_6.Ces algorithmes s'appuient sur la caractérisation des abstractions booléennes pour les systèmes d'équations linéaires issue de la première contribution. Le lien entre ces abstractions est défini en logique du premier-ordre, tel que l'abstraction peut être calculée par la programmation par contraintes sur les domaines finis également.Nous avons implémenté nos algorithmes exacts et les avons appliqués à la prédiction de knock-outs de gènes qui peuvent mener à une surproduction de leucine dans B.~Subtilis, nécessaire pour la surproduction de surfactine en biotechnologie.Le calcul des prédictions précises avec l'algorithme exact peut tout de même prendre plusieurs heures. Pour cela, nous présentons aussi une nouvelle heuristique, basée sur les modes élémentaires, pour le calcul de l'abstraction de différences. Celle-ci fournit un bon compromis entre précision et efficacité en temps.