Résolution de Contraintes Temporelles pour l'Analyse de Systèmes Biologiques
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
Temporal logics have proven useful as specification languages for describing the behavior of a broad variety of Systems ranging from electronic circuits to software programs, and more recently biological Systems. Finding mathematical models satisfying a specification built from the formalization of biological experiments is a common task of the modeler. We show that the formalization of biological temporal properties of Systems, as observed in experiments, in temporal logics specifications enable the transposition of programming concepts and tools, like model-checking, to the analysis of living processes at the cellular level. Also as temporal logics allow one to express both qualitative and quantitative information they are well suited to the increasingly quantitative, yet incomplete, uncertain and imprecise information now accumulated in the field of quantitative Systems biology. However the usual binary evaluation of temporal logic formulas is not adapted to several problems such as parameter search and quantitative robustness analysis. We show that temporal logic constraint solving enables the definition of a continuous degree of satisfaction of temporal logic formula and how it can be used as a fitness function for continuous optimization methods to provide an efficient parameter search procedure for biochemical reaction networks with respect to temporal specifications. Then we describe how we can use such a satisfaction measure for the robustness analysis and sensitivity analysis of biological models. Finally we apply these methods on several biological problems.
Abstract FR:
La logique temporelle est utilisée avec succès pour formaliser les propriétés de circuits électroniques, de logiciels, et plus récemment de systèmes biologiques. Décrire de manière formelle un modèle biologique mais aussi ses propriétés biologiques ouvre de grandes possibilités de conception d'outils automatisés aidant le modélisateur à concevoir et valider ses modèles. De plus les logiques temporelles procurent un niveau de description adapté aux données biologiques quantitatives incomplètes et imprécises. Cependant l'évaluation booléenne classique de formules de logique temporelle n'est pas adaptée à de nombreux problèmes comme la recherche de paramètres ou l'analyse quantitative de la robustesse. Nous montrons que la résolution de contraintes de logique temporelle permet la définition d'un degré de satisfaction continu de formules de logique temporelle adapté à ces problèmes. En particulier l'utilisation de ce degré de satisfaction continu comme fonction objectif ouvre la voie à l'utilisation de méthodes d'optimisation continues pour chercher de manière efficace des paramètres cinétiques satisfaisant des propriétés biologiques formalisées en logique temporelle. Ainsi après avoir étendu le model-checking en problème de résolution de contraintes de logique temporelles et permis la définition d'un degré de satisfaction continu de formules nous présentons les applications à la biologie des systèmes au travers de la recherche de paramètres, l'analyse de robustesse et l'analyse de sensibilité. Ces méthodes sont enfin évaluées sur plusieurs exemples biologiques.