Author name cluster

François Fages

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

15 papers

2 author rows

TCS Journal 2024 Journal Article

A skin microbiome model with AMP interactions and analysis of quasi-stability vs stability in population dynamics

Eléa Thibault Greugny
François Fages
Ovidiu Radulescu
Peter Szmolyan
Georgios N. Stamatas

The skin microbiome plays an important role in the maintenance of a healthy skin. It is an ecosystem, composed of several species, competing for resources and interacting with the skin cells. Imbalance in the cutaneous microbiome, also called dysbiosis, has been correlated with several skin conditions, including acne and atopic dermatitis. Generally, dysbiosis is linked to colonization of the skin by a population of opportunistic pathogenic bacteria. Treatments consisting in non-specific elimination of cutaneous microflora have shown conflicting results. In this article, we introduce a mathematical model based on ordinary differential equations, with 2 types of bacteria populations (skin commensals and opportunistic pathogens) and including the production of antimicrobial peptides to study the mechanisms driving the dominance of one population over the other. By using published experimental data, assumed to correspond to the observation of stable states in our model, we reduce the number of parameters of the model from 13 to 5. We then use a formal specification in quantitative temporal logic to calibrate our model by global parameter optimization and perform sensitivity analyses. On the time scale of 2 days of the experiments, the model predicts that certain changes of the environment, like the elevation of skin surface pH, create favorable conditions for the emergence and colonization of the skin by the opportunistic pathogen population, while the production of human AMPs has non-linear effect on the balance between pathogens and commensals. Surprisingly, simulations on longer time scales reveal that the equilibrium reached around 2 days can in fact be a quasi-stable state followed by the reaching of a reversed stable state after 12 days or more. We analyze the conditions of quasi-stability observed in this model using tropical algebraic methods, and show their non-generic character in contrast to slow-fast systems. These conditions are then generalized to a large class of population dynamics models over any number of species.

Details DOI

TCS Journal 2024 Journal Article

On a model of online analog computation in the cell with absolute functional robustness: Algebraic characterization, function compiler and error control

Mathieu Hemery
François Fages

The Turing completeness of continuous Chemical Reaction Networks (CRNs) states that any computable real function can be computed by a continuous CRN on a finite set of molecular species, possibly restricted to elementary reactions, i. e. with at most two reactants and mass action law kinetics. In this paper, we introduce a more stringent notion of robust online analog computation, called Absolute Functional Robustness (AFR), for the CRNs that stabilize the concentration values of some output species to the result of one function of the input species concentrations, while allowing arbitrary perturbations for intermediate and output species throughout the attraction basin. We prove that the set of real functions stabilized by a CRN with mass action law kinetics is precisely the set of real algebraic functions. Based on this result, we present a compiler which takes as input any algebraic function (defined by one polynomial and one point for selecting one branch of the algebraic curve defined by the polynomial) and generates an abstract CRN to stabilize it. Furthermore, we provide error bounds to estimate and control the error of an unperturbed system, under the assumption that the environment inputs are driven by k-Lipschitz functions.

Details DOI

ICLR Conference 2023 Conference Paper

Neural-based classification rule learning for sequential data

Marine Collery
Philippe Bonnard
François Fages
Remy Kusters

Discovering interpretable patterns for classification of sequential data is of key importance for a variety of fields, ranging from genomics to fraud detection or more generally interpretable decision-making. In this paper, we propose a novel differentiable fully interpretable method to discover both local and global patterns (i.e. catching a relative or absolute temporal dependency) for rule-based binary classification. It consists of a convolutional binary neural network with an interpretable neural filter and a training strategy based on dynamically-enforced sparsity. We demonstrate the validity and usefulness of the approach on synthetic datasets and on an open-source peptides dataset. Key to this end-to-end differentiable method is that the expressive patterns used in the rules are learned alongside the rules themselves.

Details

TCS Journal 2015 Journal Article

Inferring reaction systems from ordinary differential equations

François Fages
Steven Gay
Sylvain Soliman

In Mathematical Biology, many dynamical models of biochemical reaction systems are presented with Ordinary Differential Equations (ODE). Once kinetic parameter values are fixed, this simple mathematical formalism completely defines the dynamical behavior of a system of biochemical reactions and provides powerful tools for deterministic simulations, parameter sensitivity analysis, bifurcation analysis, etc. However, without requiring any information on the reaction kinetics and parameter values, various qualitative analyses can be performed using the structure of the reactions, provided the reactants, products and modifiers of each reaction are precisely defined. In order to apply these structural methods to parametric ODE models, we study a mathematical condition for expressing the consistency between the structure and the kinetics of a reaction, without restricting to Mass Action law kinetics. This condition, satisfied in particular by standard kinetic laws, entails a remarkable property of independence of the influence graph from the kinetics of the reactions. We derive from this study a heuristic algorithm which, given a system of ODEs as input, computes a system of reactions with the same ODE semantics, by inferring well-formed reactions whenever possible. We show how this strategy is capable of automatically curating the writing of ODE models in SBML, and present some statistics obtained on the model repository biomodels. net.

Details DOI

TCS Journal 2011 Journal Article

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

Aurélien Rizk
Grégory Batt
François Fages
Sylvain Soliman

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 define 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. We also show how it can be used to define a measure of robustness of a biological model with respect to some temporal specification. These methods are evaluated on models of the cell cycle and of the MAPK signaling cascade.

Details DOI

TCS Journal 2011 Journal Article

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

Elisabetta De Maria
François Fages
Aurélien Rizk
Sylvain Soliman

In systems biology, the number of available models of cellular processes has increased 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. This constraint-based approach to computing with partial information is illustrated through the design of a complex model of the mammalian cell cycle, the circadian clock, the p53/Mdm2 DNA-damage repair system, the metabolism of irinotecan and the control of cell exposure to it. We discuss the use of this model for cancer chronotherapies and evaluate its predictive power with respect to circadian core gene knock-outs.

Details DOI

TCS Journal 2008 Journal Article

Abstract interpretation and types for systems biology

François Fages
Sylvain Soliman

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. More specifically, we consider the Systems Biology Markup Language SBML, and the Biochemical Abstract Machine BIOCHAM with its differential, stochastic, discrete and boolean semantics. We first show how all of these different semantics, except the differential one, can be formally related by simple Galois connections. Then we define three type systems: one for checking or inferring the functions of proteins in a reaction model, one for checking or inferring the activation and inhibition effects of proteins in a reaction model, and another one for checking or inferring the topology of compartments or locations. We show that the framework of abstract interpretation elegantly applies to the formalization of these further abstractions, and to the implementation of linear or quadratic time type checking as well as type inference algorithms. Furthermore, we show a theorem of independence of the graph of activation and inhibition effects from the kinetic expressions in the reaction model, under general conditions. Through some examples, we show that the analysis of biochemical models by type inference provides accurate and useful information. Interestingly, such a mathematical formalization of the abstractions commonly used in systems biology already provides some guidelines for the extensions of biochemical reaction rule languages.

Details DOI

TCS Journal 2008 Journal Article

On temporal logic constraint solving for analyzing numerical data time series

François Fages
Aurélien Rizk

Temporal logics and model-checking have proved successful in expressing biological properties of complex biochemical systems, and automatically verify their satisfaction, in both qualitative and quantitative models. In this article, we go beyond model-checking and present a constraint solving algorithm for quantifier-free first-order temporal logic formulae, with constraints over the reals. This algorithm computes the domain of the real valued variables occurring in a formula that makes it true in a model. We illustrate this approach for the automatic generation of a temporal logic specification from biological data time series. We provide a set of biologically relevant patterns of formulae, and apply them to numerical data time series of models of the cell cycle control and MAPK signal transduction. We show in these examples that this approach infers automatically semi-qualitative, semi-quantitative information about concentration thresholds, amplitude of oscillations, stability properties, checkpoints and influences between species.

Details DOI

LOPSTR Conference 2005 Conference Paper

Temporal Logic Constraints in the Biochemical Abstract Machine BIOCHAM

François Fages

Abstract Recent progress in Biology and data-production technologies push research toward a new interdisciplinary field, named Systems Biology, where the challenge is to break the complexity walls for reasoning about large biomolecular interaction systems. Pioneered by Regev, Silverman and Shapiro, the application of process calculi to the description of biological processes has been a source of inspiration for many researchers coming from the programming language community. In this presentation, we give an overview of the Biochemical Abstract Machine (BIOCHAM), in which biochemical systems are modeled using a simple language of reaction rules, and the biological properties of the system, known from experiments, are formalized in temporal logic. In this setting, the biological validation of a model can be done by model-checking, both qualitatively and quantitatively. Moreover, the temporal properties can be turned into specifications for learning modifications or refinements of the model, when incorporating new biological knowledge.

Details

TCS Journal 2004 Journal Article

Modeling and querying biomolecular interaction networks

Nathalie Chabrier-Rivier
Marc Chiaverini
Vincent Danos
François Fages
Vincent Schächter

We introduce a formalism to represent and analyze protein–protein and protein–DNA interaction networks. We illustrate the expressivity of this language, by proposing a formal counterpart of Kohn's compilation on the mammalian cell-cycle control. This effectively turns an otherwise static knowledge into a discrete transition system incorporating a qualitative description of the dynamics. We then propose to use the computation tree logic (CTL) as a query language for querying the possible behaviors of the system. We provide examples of biologically relevant queries expressed in CTL about the mammalian cell-cycle control and show the effectiveness of symbolic model checking tools to evaluate CTL queries in this context.

Details DOI

I&C Journal 2001 Journal Article

Linear Concurrent Constraint Programming: Operational and Phase Semantics

François Fages
Paul Ruet
Sylvain Soliman

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.

Details DOI

CSL Conference 1998 Conference Paper

Concurrent Constraint Programming and Non-commutative Logic

Paul Ruet
François Fages

Abstract This paper presents a connection between the intuitionistic fragment of a non-commutative version of linear logic introduced by the first author (NLI) and concurrent constraint programming (CC). We refine existing logical characterizations of operational aspects of CC, by providing a logical interpretation of finer observable properties of CC programs, namely stores, successes and suspensions.

Details

TCS Journal 1997 Journal Article

Combining explicit negation and negation by failure via Belnap's logic

Paul Ruet
François Fages

This paper deals with logic programs containing two kinds of negation: negation as failure and explicit negation. This allows two different forms of reasoning in the presence of incomplete information. Such programs have been introduced by Gelfond and Lifschitz and called extended programs. We provide them with a logical semantics in the style of Kunen, based on Belnap's four-valued logic, and an answer sets' semantics that is shown to be equivalent to that of Gelfond and Lifschitz. The proofs rely on a translation into normal programs, and on a variant of Fitting's extension of logic programming to bilattices.

Details DOI

TCS Journal 1993 Journal Article

Average-case analysis of unification algorithms

Luc Albert
Rafael Casas
François Fages

Unification in first-order languages is a central operation in symbolic computation and logic programming. Many unification algorithms have been proposed in the past; however, there is no consensus on which algorithm is the best to use in practice. While Paterson and Wegman's linear unification algorithm (1978) has the lowest time complexity in the worst case, it requires an important overhead to be implemented. This is true also, although less importantly, for Martelli and Montanari's algorithm (Martelli and Montanari 1982), and Robinson's algorithm (Robinson 1971), is finally retained in many applications despite its exponential worst-case time complexity. In this paper, we present unification algorithms in a uniform way and provide average-case complexity theoretic arguments. We estimate the number of unifiable pairs of trees. We analyse the different reasons for failure and get asymptotical and numerical evaluations. We then extend the previous results of Dershowitz and Lindenstrauss (1989) to these families of trees and show that a slight modification of Herbrand-Robinson's algorithm has a constant average cost on random pairs of trees. On the other hand, we show that various variants of Martelli and Montanari's algorithm all have a linear average cost on random pairs of trees. The reason is that failures by clash are not sufficient to lead to a constant average cost; an efficient occur check, i. e. without a complete traversal of subterms, is necessary. In the last section, we present a combinatorial extension of the problem for terms formed over a countable set of variables, and extend to this framework the results on the probability of the occur-check.

Details DOI

TCS Journal 1986 Journal Article

Complete sets of unifiers and matchers in equational theories

François Fages
Gérard Huet

We propose an abstract framework to present unification and matching problems. We argue about the necessity of a somewhat complicated definition of a basis of unifiers. In particular, we prove the nonexistence of complete sets of minimal unifiers (and matchers) in some equational theories, even regular.

Details DOI