François Fages

Hybrid Simulations of Heterogeneous Biochemical Models in SBML

Wed, Apr 1, 2015

A constraint solving approach to model reduction by tropical equilibration

Model reduction is a central topic in systems biology and dynamical systems theory, for reducing the complexity of detailed models, finding important parameters, and developing multi-scale models for instance. While singular perturbation theory is a standard mathematical tool to analyze the different time scales of a dynamical system and decompose the system accordingly, tropical methods provide a simple algebraic framework to perform these analyses systematically in polynomial systems. The crux of these methods is in the computation of tropical equilibrations […]

Mon, Dec 1, 2014

Trace Simplifications preserving Temporal Logic Formulae with Case Study in a Coupled Model of the Cell Cycle and the Circadian Clock (Best Student Paper Prize)

Best student paper award

Sat, Nov 1, 2014

On the subgraph Epimorphism Problem

In this paper we study the problem of deciding the existence of a subgraph epimorphism between two graphs. Our interest in this variant of graph matching problem stems from the study of model reductions in systems biology, where large systems of biochemical reactions can be naturally represented by bipartite digraphs of species and reactions. In this setting, model reduction can be formalized as the existence of a sequence of vertex deletion and merge operations that transforms a first reaction graph into a second graph […]

Wed, Jan 1, 2014

Solving Subgraph Epimorphism Problems using CLP and SAT

In this work, we compare CLP and SAT solvers on the NP-complete problem of deciding the existence of a subgraph epimorphism between two graphs. Our interest in this variant of graph matching problem stems from the study of model reductions in systems biology, where large systems of biochemical reactions can be naturally represented by bipartite digraphs of species and reactions. In this setting, model reduction can be formalized as the existence of a sequence of vertex, species or reaction, deletion and merge operations which transforms a first reaction graph into a second graph […]

Sun, Sep 1, 2013

On the Hybrid Composition and Simulation of Heterogeneous Biochemical Models

Models of biochemical systems presented as a set of formal reaction rules with kinetic expressions can be interpreted with different semantics: as either deterministic Ordinary Differential Equations, stochastic continuous-time Markov Chains, Petri nets or Boolean transition systems. While the formal composition of reaction models can be syntactically defined as the (multiset) union of the reactions, the hybrid composition of models in different formalisms is a largely open issue. In this paper, we show that the combination of reaction rules with conditional events, as the ones already present in SBML, does provide the expressive power of hybrid automata and can be used in a non standard way to give meaning to the hybrid composition of heterogeneous models of biochemical processes […]

Sun, Sep 1, 2013

A Constraint Solving Approach to Tropical Equilibration and Model Reduction

Model reduction is a central topic in systems biology and dynamical systems theory, for reducing the complexity of detailed models, finding important parameters, and developing multi-scale models for instance. While perturbation theory is a standard mathematical tool to analyze the different time scales of a dynamical system, and decompose the system accordingly, tropical methods provide a simple algebraic framework to perform these analyses systematically in polynomial systems. The crux of these tropicalization methods is in the computation of tropical equilibrations […]

Sun, Sep 1, 2013

Un modèle booléen pour l'énumération des siphons et des pièges minimaux dans les réseaux de Petri

Petri-nets are a simple formalism for modeling concurrent computation. Recently, they have emerged as a powerful tool for the modeling and analysis of biochemical reaction networks, bridging the gap between purely qualitative and quantitative models. These networks can be large and complex, which makes their study difficult and computationally challenging […]

Tue, May 1, 2012

Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures

Finding mathematical models satisfying a specification built from the formalization of biological experiments, is a common task of the modeler that techniques like model-checking help solving, in the qualitative but also in the quantitative case. In this article we go one step further by defining a continuous degree of satisfaction of temporal logic formulae with constraints. We show how such a satisfaction measure can be used as a fitness function with state-of-the-art evolutionary optimization methods in order to find biochemical kinetic parameter values satisfying a set of biological properties formalized in temporal logic […]

Wed, Jun 1, 2011

Design, optimization and predictions of a coupled model of the cell cycle, circadian clock, DNA repair system, irinotecan metabolism and exposure control under temporal logic constraints

In systems biology, the number of available models of cellular processes increases rapidly, but re-using models in different contexts or for different questions remains a challenging issue. In this paper, we study the coupling of different models playing a role in the mammalian cell cycle and in cancer therapies. We show how the formalization of experimental observations in temporal logic with numerical constraints can be used to compute the unknown coupling kinetics parameter values agreeing with experimental data […]

Sun, May 1, 2011

A graphical method for reducing and relating models in systems biology

Motivation: In Systems Biology, an increasing collection of models of various biological processes is currently developed and made available in publicly accessible repositories, such as biomodels.net for instance, through common exchange formats such as SBML. To date, however, there is no general method to relate different models to each other by abstraction or reduction relationships, and this task is left to the modeler for re-using and coupling models. In mathematical biology, model reduction techniques have been studied for a long time, mainly in the case where a model exhibits different time scales, or different spatial phases, which can be analyzed separately […]

Wed, Sep 1, 2010

Abstract interpretation and types for systems biology

Abstract interpretation is a theory of abstraction that has been introduced for the analysis of programs. In particular, it has proved useful for organizing the multiple semantics of a given programming language in a hierarchy corresponding to different detail levels, and for defining type systems for programming languages and program analyzers in software engineering. In this paper, we investigate the application of these concepts to systems biology formalisms […]

Fri, Aug 1, 2008

Langages formels dans la machine abstraite biochimique BIOCHAM

Le développement de langages formels pour modéliser les systèmes biologiques ouvre la voie à la conception de nouveaux outils de raisonnement automatique destinés au biologiste modélisateur. La machine abstraite biochimique BIOCHAM est un environnement logiciel qui offre un langage simple de règles pour modéliser des interactions biomoléculaires, et un lan-gage puissant fondé sur la logique temporelle pour formaliser les propriétés biologiques du sys-tème. En s'appuyant sur ces deux langages formels, il devient possible d'utiliser des techniques d'apprentissage automatique pour inférer de nouvelles règles de réaction, estimer les valeurs des paramètres cinétiques, et corriger ou compléter les modèles semi-automatiquement […]

Sat, Dec 1, 2007

Closures and Modules Within Linear Logic Concurrent Constraint Programming

There are two somewhat contradictory ways of looking at modules in a given programming language. On the one hand, module systems are largely independent of the particulars of programming languages. On the other hand, the module constructs may interfere with the programming constructs, and may be redundant with the other scope mechanisms of a specific programming language, such as closures for instance […]

Sat, Dec 1, 2007

Machine Learning Biochemical Networks from Temporal Logic Properties

One central issue in systems biology is the definition of formal languages for describing complex biochemical systems and their behavior at different levels. The biochemical abstract machine BIOCHAM is based on two formal languages, one rule-based language used for modeling biochemical networks, at three abstraction levels corresponding to three semantics: boolean, concentration and population; and one temporal logic language used for formalizing the biological properties of the system. In this paper, we show how the temporal logic language can be turned into a specification language […]

Fri, Dec 1, 2006

BIOCHAM: an environment for modeling biological systems and formalizing experimental knowledge

BIOCHAM (the BIOCHemical Abstract Machine) is a software environment for modeling biochemical systems. It is based on two aspects: (1) the analysis and simulation of boolean, kinetic and stoch-astic models and (2) the formalization of biological properties in temporal logic. BIOCHAM provides tools and languages for describing protein networks with a simple and straightforward syntax, and for integrating biological properties into the model […]

Sat, Apr 1, 2006

CLPGUI: A Generic Graphical User Interface for Constraint Logic Programming

CLPGUI is a generic graphical user interface for visualizing and controlling the execution of constraint logic programs. CLPGUI has been designed to be used in different contexts: initially for teaching purposes, then for debugging complex programs of real-world scale, and recently for developing end-user interfaces. The challenge of developing a tool which is generic w.r.t […]

Fri, Oct 1, 2004

Linear Concurrent Constraint Programming: Operational and Phase Semantics

In this paper we give a logical semantics for the class CC of concurrent constraint programming languages and for its extension LCC based on linear constraint systems. Besides the characterization in intuitionistic logic of the stores of CC computations, we show that both the stores and the successes of LCC computations can be characterized in intuitionistic linear logic. We illustrate the usefulness of these results by showing with examples how the phase semantics of linear logic can be used to give simple semantical" proofs of safety properties of LCC programs […]

Thu, Feb 1, 2001