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

Change predictions for reaction networks with partial kinetic information can be obtained by qualitative reasoning with abstract interpretation. A typical change prediction problem in systems biology is which gene knockouts may, or must, increase the outflow of a target species at a steady state. Answering such questions for reaction networks requires reasoning about abstract differences such as "increases'' and "decreases''. A task fundamental for change predictions was introduced by Niehren, Versari, John, Coutte, et Jacques (2016). It is the problem to compute for a given system of linear equations with nonlinear difference constraints, the difference abstraction of the set of its positive solutions. Previous approaches provided overapproximation algorithms for this task based on various heuristics, for instance by rewriting the linear equations. In this thesis, we present the first algorithms that can solve this task exactly for the two difference abstractions used in the literature so far. As a first contribution, we show how to characterize for a linear equation system the boolean abstraction of its set of positive solutions. This abstraction maps any strictly positive real numbers to 1 and 0 to 0. The characterization is given by the set of boolean solutions for another equation system, that we compute based on elementary modes. The boolean solutions of the characterizing equation system can then be computed based on finite domain constraint programming in practice. We believe that this result is relevant for the analysis of functional programs with linear arithmetics. As a second contribution, we present two algorithms that compute for a given system of linear equations and nonlinear difference constraints, the exact difference abstraction into Delta_3 and Delta_6 respectively. These algorithms rely on the characterization of boolean abstractions for linear equation systems from the first contribution. The bridge between these abstractions is defined in first-order logic. In this way, the difference abstraction can be computed by finite set constraint programming too. We implemented our exact algorithms and applied them to predicting gene knockouts that may lead to leucine overproduction in B.~Subtilis, as needed for surfactin overproduction in biotechnology. Computing the precise predictions with the exact algorithm may take several hours though. Therefore, we also present a new heuristics for computing difference abstraction based on elementary modes, that provides a good compromise between precision and time efficiency.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