Construction de modèle par résolution de contraintes de logique temporelle : étude du couplage entre le cycle cellulaire et l’horloge circadienne

In this dissertation, we explore the use of temporal logic and model checking in systems biology. Our thesis is that temporal logic provides a powerful language to formalize complex yet imprecise dynamical properties of biological systems and to partly automate model building as a constraint satisfaction problem. We take advantage of this logical paradigm for systems biology to capture properties emerging from complex regulatory networks. First, we investigate the ability of Computation Tree Logic to verify dynamical properties in asynchronous state transition graphs derived from logical models of the mammalian cell cycle. Logical modeling provides a qualitative and potentially non-deterministic description of a biological system. This feature is useful to account for a variety of dynamical properties, observed in different conditions within a generic model. We develop an approach of iterative property verification to assist the building and updating of logical models. Then we consider quantitative deterministic models. For such models, oscillatory properties such as pseudo-periods and pseudo-phases are formalized by quantitative constraints in First-Order Linear Time Logic. A continuous model can provide a precise description of the mechanisms governing a complex regulatory network, and a quantitative prediction of its dynamics. However, the classical difficulties associated with this approach are brought by numerous and often poorly characterized kinetic parameters. We address this challenge by im- plementing two complementary strategies to obtain efficient solving of dynamical constraints over a finite time horizon: the design of useful temporal logic formula patterns associated with dedicated constraint solvers, and some trace simplification rules to safely reduce the size of the traces to analyze. We show that this approach enables the calibration of high-dimensional models on quantitative single-cell data with an application to model coupling for the mammalian cell cycle and the circadian clock. Understanding the relationships between these two molecular oscillators is an important problem in the field of chronobiology. We draw several coupling hypotheses and investigate their consequences.Cette dissertation explore l’utilisation de la logique temporelle et de la vérification de mod- èle en biologie des systèmes. Nous soutenons que la logique temporalle constitue un outil puis- sant pour formaliser des propriétés dynamiques à la fois complexes et imprécises permettant de caractériser un système biologique. Cet outil peut être utilisé pour partiellement automatiser la construction de modèle, comme une résolution d’un problème de satisfaction de contraintes. Tout d’abord, nous étudions l’emploi de la logique arborecente (Computation Tree Logic) pour vérifier des propriétés dynamiques dans des graphes de transitions d’états discrets asyn- chrones, dérivés de modèles logiques du cycle cellulaire mammifère. La modélisation logique fournit une description qualitative et potentiellement non-déterministe d’un système biologique. Elle offre un cadre utile pour rendre compte des diverses propriétés dynamiques observées dans différentes conditions au sein d’un modèle générique. Nous développons une approche de vérification itérative de propriétés pour assister la construction et la mise à jour de modèles logiques. Puis, nous considérons des modèles quantitatifs déterministes. Pour de tels modèles, des propriétés sur les oscillations, telles que pseudo-période ou pseudo-phase, peuvent être formalisées par des contraintes quantitatives en logique du premier ordre à temps linéaire (First- Order Linear Time Logic, FO-LTL). Un modèle continu peut fournir une description précise des mécanismes impliqués dans un réseau de régulations complexe, ainsi qu’une prédiction quan- titative de ses dynamiques. Cependant, une difficulté bien connue associée à cette approche provient du grand nombre de paramètres cinétiques, qui sont souvent mal caractérisés. Afin de répondre à ce problème, nous implémentons deux stratégies complémentaires pour améliorer l’efficacité de la résolution de contraintes dynamiques sur un horizon de temps fini. Une première approche exploite la définition d’une liste de motifs de logique temporelle fréquemment utilisés, associés à des solveurs de contraintes dédiés. Dans la deuxième approche, nous définissons et appliquons des règles de simplification de trace permettant de réduire la trace à analyser sans perte d’information. Nous montrons que cette approche permet de calibrer des modèles de haute dimension sur des données quantitatives sur cellule individuelle. Elle est appliquée au couplage de modèles du cycle cellulaire et de l’horloge circadienne mammifères. Comprendre la relation entre ces deux rythmes moléculaires est un problème important dans le domaine de la chronobiologie. Nous déduisons différentes hypothèses de couplage et étudions leurs conséquences