http://contraintes.inria.fr/Seminar
Monday 24 October 2011
10.30 Neda Saeedloei, University of
Texas, Dallas,
USA
Modeling and Verification of Real-time
and Cyber-Physical Systems
We develop techniques for including continuous time in computations.
These techniques result in frameworks for modeling and verification of
real-time systems. Our proposed framework is based on logic programming
(LP) extended with constraints and coinduction. To build the
theoretical foundations necessary for this work, we present a new
programming paradigm, co-constraint logic programming (co-CLP for
brevity), that merges two programming paradigms: constraint logic
programming and coinductive logic programming.
We investigate incorporation of continuous time in various domains of
computer science. In particular we study the extension of
omega-grammars with continuous time (timed omega-grammars) and also
continuous time extension of pi-calculus (timed pi-calculus). We
present the implementation of these formalisms in co-CLP and show how
these co-CLP-based realizations can be used for modeling and verifying
real-time systems.
We also present a co-CLP framework for modeling hybrid automata; we use
this logic programming realization of hybrid automata to develop a
framework for modeling and verification of cyber-physical systems,
including real-time systems.
Monday 10 October 2011 (Seminar room of Building 16)
10.00 Calin Belta, Boston University,
USA
Formal verification and control of
piecewise affine systems with applications to gene networks
Discrete-time piecewise affine systems (PWA) are a particular class of
hybrid systems
that evolve along different affine dynamics in different polyhedral
regions of the continuous state space. Such models are very popular
because they can approximate nonlinear systems with arbitrary accuracy
and because of the existence of algorithms for the identification of
such systems from experimental data. In this talk, I will show how the
particular structure of PWA systems can be exploited to develop
computationally efficient algorithms for their verification and for
synthesis of parameters and control strategies. I will show how such
tools can be used for analysis and synthesis of synthetic gene
networks.
Jeudi 21 avril 2011
10.00 Szymon Stoma, Humboldt
University, Berlin, Germany
Towards systematic study of
spatio-temporal cellular systems
During the presentation I will discuss the application of computational
techniques to study complex, spatio-temporal cellular systems. I will
present models and simulations together with experiments used to
heighten our comprehension of shoot apical meristem (SAM) development
in Arabidopsis Thaliana, and in particular the process of regular organ
initiation, called phyllotaxis. To develop phyllotaxis models, we
focused on the intra cellular transport of one of the essential plant
hormones, auxin. Transport of auxin is mediated by its efflux carrier,
a protein called PIN1. The location of PIN proteins in a single cell
changes dynamically during the growth process and this so-called
repolarization is coordinated at a tissue level. To capture these
events, presented models are at the scale of tissue, with cellular
resolution and since they include growth, from the Computer Science
point of view they are Dynamic Systems with Dynamic Structures (DS2),
which brings important implications to the modeling. I will discuss
also the physical-based framework to simulate growth of the meristem
including tropisms. Since auxin modifies rigidity of cell walls leading
to an increase in growth rates in the spots of its high concentration,
the introduced framework is used to upgrade auxin transport-based model
of phyllotaxis. In this upgraded model the transport-based patterning
mechanism directly modifies the growth directions of the meristem,
allowing us to study the coupling of growth, auxin and PIN
distributions. Finally, I will discuss the usage of experimental,
microscopic data to validate microbiological models which will bring us
to the motivation for developing Spatio Temporal Simulation Environment
(STSE): http://stse-software.org
Lundi 18 avril 2011
13.30 Cédric Joncour,
Université Bordeaux 1
Nouvelles approches combinatoires pour les problèmes de
placement
Le problème de placement sur deux dimensions consiste à
décider s'il existe un rangement d'objets rectangulaires dans
une boîte donnée sans chevauchement ni dépassement
du conteneur. C'est un problème combinatoire très
difficile. La rotation des rectangles n’est pas autorisée. En
1997, Fekete et Schepers ont utilisé les graphes d’intervalles
comme structure de données afin de caractériser des
classes de placements réalisables. Ils évitent ainsi
d’énumérer des solutions symétriques. Leur
algorithme a permis de faire un saut significatif quant à la
taille des instances traitées.
Durant ma thèse, j'ai developpé de nouvelles approches
combinatoires basées sur diverses caractérisations des
graphes d'intervalles. Un premier algorithme est basé sur
l'énumération de matrices de uns-consécutifs. Un
autre utilise des arbres étiquetés pour éliminer
plus efficacement les cas de symétries entre placements. Ces
approches se sont révélées plus performantes que
celle de Fekete & Schepers sur la plupart des instances classiques
de la littérature.
Lundi 11 avril 2011
14.00 Paolo Ballarini, INRIA Rennes
Bretagne Atlantique,
Hybrid Automata Stochastic Logic:
expressive statistical verification of stochastic models
We introduce the Hybrid Automata Stochastic Logic (HASL), a new
temporal logic formalism for the verification of discrete event
stochastic processes (DESP).
HASL employs Linear Hybrid Automata (LHA) as machineries to select
prefixes of relevant execution paths of a DESP. The advantage with LHA is that
rather elaborate information can be collected "on-the-fly" during path
selection, providing the user with a powerful means to express sophisticated measures. A formula of HASL consists of an LHA
(A) and an expression (Z) referring to moments of "path random
variables". A (simulation-based)
statistical engine is employed to obtain a confidence-interval estimate
of the expected value of Z. In
essence HASL provides a unifying verification framework where
sophisticated temporal reasoning is naturally blended with elaborate reward-based
analysis. In this talk I will
illustrate the HASL approach and a discuss about its expressivity. I will also present preliminary
empirical evidence obtained through COSMOS, a prototype software tool
for HASL verification.
(slides in pdf)
Lundi 28 mars 2011
10.30 Yaakov Setty, Weizmann
Institute, Revohot,
Israel,
Modeling Organogenesis: Scaling Development from Stem Cells to Organs
In recent years, we have used software engineering tools to develop
reactive models to simulate and analyze the development of organs. The
modeled systems embody highly complex and dynamic processes, by which a
set of precursor stem cells proliferate, differentiate and move, to
form a functioning tissue. Three organs from diverse evolutionary
organisms have been thus modeled: the mouse pancreas, the C. elegans
gonad, and partial rodent brain development. Analysis and execution of
the models provided dynamic representation of the development,
anticipated known experimental results and proposed novel testable
predictions. In my talk, I will l discuss challenges, goals and
achievement in this direction in science.
Mardi 1er mars 2011
10.00 Xuefeng Gao, University College,
Cork, Ireland,
A cell-based multiscale model for avascular tumor growth
The growth dynamics of tumors is controlled by nutrients, biomechanical
forces and other factors at different stages and in different
environments is still largely unknown. We present a computer simulation
for avascular tumor growth aimed at investigating the interaction
between tumor morphology and the local environment. At the cellular
level, a Glazier-Graner-Hogeweg (GGH) model describes cellular dynamics
including cell proliferation, viability and adhesion. At the
subcellular level, the expression of protein p27 regulates the cell
cycle. At the extracellular level, the diffusion of oxygen, glucose and
hydrogen ions describe the chemical dynamics involved in metabolism. In
avascular phase, tumor cell proliferation depends on consuming oxygen
and glucose from the pre-existing surrounding tissue. When the oxygen
level drops below a threshold, the tumor cells become hypoxic and start
anaerobic metabolism (glycolysis). Experimental evidence suggests that
cancer cells undergo hypoxia-induced quiescence (G0 phase in the cell
cycle). We assume that this progression is affected by protein p27,
whose expression is upregulated under hypoxia, inhibits the activation
of the cyclin dependent kinases (CDKs), thus preventing DNA synthesis
and regulating the cell-cycle.
Mercredi 8 décembre 2010
11.00-12.00 (amphi Turing, building 1)
Radu Grosu, SUNY at Stony Brook, USA
Modeling and Analysis of Cardiac Tissue
We address the problem of modeling and analysis of emergent behavior
in cardiac tissue, spiral electric waves in particular, a condition
known as tachycardia and a precursor to cardiac fibrillation.
We first introduce a minimal nonlinear model of a single cardiac cell.
For analysis, we transform this model to a multiaffine system and
identify the parameter ranges for which the system lacks excitability.
A region of unexcitable cells within cardiac tissue, can be responsible
for tachycardia or fibrillation: 1) The region becomes an obstacle, in
the way of the propagating electrical wave; 2) This triggers a spiral
rotation of the wave (tachycardia); 3) The spiral may eventually break
up into many spirals, a condition known as fibrillation.
We then address the problem of specifying and detecting spatial
properties in cardiac tissue. To solve this problem we: (1) Apply
discrete mode-abstraction to the single-cell automata described above;
(2) Introduce the new concept of spatial-superposition of CLHA modes;
(3) Develop a new spatial logic, based on spatial-superposition, for
specifying emergent behavior; (4) Devise a new method for learning the
formulae of this logic from the spatial patterns under investigation;
and (5) Apply bounded model checking to detect (within milliseconds)
the onset of spiral waves. We have implemented our methodology as the
Emerald tool-suite, a component of our EHA framework for specification,
simulation, analysis and control of excitable hybrid automata. We
illustrate the effectiveness of our approach by applying Emerald to
the scalar electrical fields produced by our CX simulator.
Vendredi 19 novembre 2010
14.00-15.00 Jean Krivine, CNRS PPS,
University Paris 7
Epigenetics, aging and symmetry: or why DNA is not a program
Without committing to
any controversial definition, one may describe
aging as a continuous and irreversible process by which molecules, cells
or organs accumulate changes in time. With this simple definition, the
process by which embryonic stem cells progressively loose their
pluripotency by differentiation and acquire fixed functions in various
tissues can be viewed as an instance of the aging process. From a
modeling perspective there is a need to find a mechanistic molecular
implementation of this phenomenon with the hope to better understand age
related deceases or cancer. This model of cell development is strongly
constrained by the fact that each cell of a single organism, be it a
neuron or a stem cell, shares a copy of the same genetic code. It
results
that the "program" that governs the function of a cell cannot be solely
contained in the genes and has to be hidden in some "meta" instructions
on top of these genes.
Recent technological breakthrough in molecular biology are starting to
reveal the structure of this meta-code that biologists call epigenetic.
In this talk we will survey this revolutionary view of genes, cells and
function with a computer-science oriented spirit, having in mind that we
are facing an evolution-based toolkit for the treatment of genetic
information that should most likely beget interesting concepts for
computer science and informatics.
15.30-16.30 Zohra Khalis, CNRS I3S,
Sophia Antipolis
Using Hoare logic for constraining parameters of discrete models of
gene networks
The technology of DNA
chips allows the quantification of the expression
level of thousands genes in the same organism at the same time.
Nevertheless, analysis of data from DNA chips requires development of
adapted methods.
We propose a path language that allows the description, in an abstract
way, of the concentration level variations from temporal data like
temporal profiles of gene expression. When concentration level
variations have been expressed through a program of the path language,
it becomes possible to apply methods from computer science like Hoare
logic.
Hoare logic is made of a system composed of axioms and rules. It permits
one to prove if a program is correct in comparison to its specifications
that is described through assertions, that is, logical formulas, that
define properties on the program. The precondition specifies the initial
state before the execution of the program and the postcondition
specifies the final state after the execution of the program. A program
is said (partially) correct if it is possible to prove that from an
initial state satisfying the precondition, the program leads (if the
program terminates) to a final state satisfying the postcondition.
To model gene regulatory networks, the main difficulty remains in the
parameter identification problem, that is, the search of parameter
values which lead to a model behavior that is consistent with the known
or hypothetical properties of the system. So, we apply a Hoare-like
logic designed for the defined path language and discrete modelling
framework. The axioms and rules of this Hoare-like logic are adapted to
gene networks and permits us to prove that the path described by the
program exists in the dynamics. Given a path program and a
postcondition, we can apply calculus of the weakest precondition, based
on this Hoare-like logic. Calculus of the weakest precondition, thanks
to defined axioms and rules, permits us to constrain parameters
associated with the program and the postcondition. Although Hoare logic
is well known, its application to constrain parameter values of gene
networks appears to be brand new and helpful in order to select
consistent models. Moreover, expressing DNA profiles into programs gives
another way to process such data.
Mercredi 31 mars 2010
10.30 Adam Halasz, West Virginia
University – Department of Mathematics
[Non]-Deterministic dynamics in cells: From multistability to
stochastic switching.
I will discuss the
interplay between deterministic dynamics and
stochastic effects in live cells. The main example is the lac operon,
a set of self-promoting genes, which, together with the enzymes they
express, act as a hysteretic switch. Stochastic simulations of the
same system predict spontaneous, random switching by individual cells.
This behavior can be well described by a simple abstraction. In a
broader context, I will review a few examples where stochasticity
leads to useful and quantifiable behavior that amounts to a hedging
strategy on the level of a population of cells.
Lundi 1er mars 2010
13.30 Vianney le Clément, UCL Louvain,
Belgique
Appariements de graphes basés sur des contraintes
Les graphes
combinatoires offrent une structure riche pour modéliser divers
objets: réseaux, images, molécules, etc. Pour mesurer la
similarité entre deux graphes, l'on peut calculer un appariement
entre leurs nœuds. La plupart des problèmes d'appariement de
graphes sont NP difficiles. Dans cet exposé, nous verrons qu'il
est possible de les résoudre en utilisant des techniques de
programmation par contraintes (CP) ou de recherche locale (LS). Nous
aurons aussi un aperçu du travail en cours sur CBGML, un langage
de modélisation déclaratif à base de contraintes,
dont le but est de générer automatiquement un algorithme
de résolution CP ou LS sur base des caractéristiques du
problème.
Mercredi 10 février 2010
10.30 Alexis Saurin, PPS Paris,
Focalisation en Ludique
La propriété de
Focalisation constitue l'un des résultats essentiels de la
théorie de la
démonstration de la logique linéaire,
mettant en évidence la notion
de polarité en logique. La Focalisation est la
source de développements
importants, allant de la programmation logique
linéaire aux approches
interactives de sémantiques de jeux. La
ludique, quant à elle, est un
formalisme logique introduit par Girard
il y a une dizaine d'années
dont l'élément de base est la notion
d'interaction.
Terui a revisité
récemment la théorie ludique de Girard en y apportant de
nouvelles perspectives,
notamment selon l'aspect
calculatoire, sous le nom de computational
ludics. Je présenterai une
analyse interactive du théorème de
focalisation menée dans le
cadre de la Ludique de Terui, que l'on peut
voir comme une internalisation de la
focalisation. J'expliquerai
également les motivations de
ce travail provenant de la
remarque que la
propriété de focalisation est connectée à
des résultats de
théorie de la complexité algorithmique.
(Travail en collaboration avec Basaldella
et Terui, RIMS, Kyoto)
Vendredi 27 novembre 2009
10.30 Christine Solnon, LIRIS Lyon,
Présidente AFPC, (transparents)
Mesurer la
similarité de graphes.
De nombreuses tâches
telles que, par exemple, la classification et la
recherche d'informations, nécessitent
de mesurer la similarité
d'objets. Lorsque les objets
sont modélisés par des graphes, il s'agit
alors de mesurer la
similarité de graphes, c'est à dire, mettre en
correspondance les sommets des
graphes de façon à retrouver un maximum
de caractéristiques communes.
Nous présenterons tout d'abord les
principales mesures de
similarité de graphes existantes, allant de
l'isomorphisme de (sous-)graphes,
aux distances d'édition, en passant
par la recherche de plus grands
sous-graphes communs. Nous
présenterons ensuite les
principales approches de résolution utilisées
pour résoudre ces
différents problèmes. Nous décrirons enfin
un
système pour mesurer la
similarité de graphes, basé sur les
contraintes : ce système
intègre un langage de haut niveau, permettant
à un utilisateur de
définir une mesure de similarité de façon
déclarative en termes de
contraintes, et un synthétiseur
d'algorithmes,
générant un algorithme de résolution adapté
au problème
décrit.
Lundi 9 novembre 2009
10.30 Nikolaus Hansen, LRI Orsay
The difficulties of black-box optimization and a stochastic variable
metric approach.
Stochastic
optimization techniques are recognized in practice as useful
complements to classical gradient based optimization methods.
Population-based stochastic optimizers, like Evolutionary Algorithms,
are not as easily trapped into local optima as gradient based methods,
because they operate synchronously with a set of solution points and do
not exploit local gradient information.
This talk will
start with defining a black-box optimization problem and discuss
properties that make a function of n continuous variables difficult to
optimize in practice. Then we will give an introduction into the
Covariance Matrix Adaptation Evolution Strategy (CMA-ES). The CMA-ES is
a mature stochastic optimization method, provided with a second order
model comparable to quasi-Newton methods in deterministic optimization.
We will explain how CMA-ES addresses the discussed difficulties and, if
time allows, we will compare the method with other deterministic and
stochastic optimization methods.
Mercredi 14 octobre 2009
14.00 Sylvain Pradalier, INRIA
Paris-Rocquencourt
Modeling, Simulating and Analyzing nano-machines in the nano-kappa calculus.
The modeling of biochemical
systems using process-algebra languages is
now a well-established domain. The main goals of this domain are to
help biologists and chemists to model, simulate and analyze their
systems by taking advantages of modelings done in a formal language.
Typical applications are computer-base simulations, model-checking or
abstract interpretation.
We focus on the study of nano-machines. Nano-machines are molecular
complexes synthesized by assembling various chemical groups in order to
achieve a predetermined task. They typically transform chemical events
into mechanical events. Because of their intrisic concurrent and
compositional nature, the modeling of such systems finds a natural
candidate in process-algebra.
I will present the nano-kappa calculus, a formalism dedicated to
this task. Molecules are the basic agents of the computation. The
stochastic dynamics of the calculus is specified in terms of reactions
which create, destroy or flip bonds between molecules and possibly
change their internal state.
I will also present the modeling of the Rotaxane RaH nano-machine and
what information where provided by the simulations we did.
I
will finally present an encoding from the nano-kappa to the
stochastic-pi calculus. We believe that reactive-based approaches like
nano-kappa are easier to understand and learn than agent-based
approaches, such as the pi-calculus, and moreover that they
provide
modelings easy to modify, reuse and compose. However the theory of the
pi-calculus is much better know, and it has more tools. The very strong
correctness of this encoding should permit to use the nano-kappa
calculus as a front-end language while keeping the benefits of the
theory of traditional process-algebra.
Vendredi 24 avril 2009
10.30 Alexis Saurin, Université
de Turin
Recherche de preuve par élimination des coupures.
Les liens entre programmation
et théorie de la démonstration (par
exemple
dans le calcul des séquents de Gentzen) sont étroits et
sont construits
principalement autour de deux correspondances:
(i) la correspondance entre programmation fonctionnelle et
élimination des
coupures,
bien connue sous le nom de correspondance de Curry-Howard;
(ii) la correspondance entre recherche de preuve et programmation
logique.
Ces deux approches sont fondées sur le Hautpsatz de Gentzen qui
affirme à la
fois
(a) la possibilité de transformer une preuve avec des coupures
en une preuve
sans
coupure -- approche (i) -- et (b) l'admissibilité de la coupure,
ie les
sytèmes de preuve
avec et sans coupure ont la même force déductive --
approche (ii).
Pour autant, ces deux approches se sont développées de
manière largement
indépendante.
Je présenterai dans cet exposé un modèle de
construction de preuve guidée
par un
processus d'élimination des coupures. Cette construction sera
basée sur la
Ludique
de Girard qui fournit les ingrédients nécessaires
à la construction.
Informellement, on verra la recherche de preuve se développer au
fur et à
mesure que
la preuve en construction se développe de manière
à répondre à des tests
(des
"objections") qui sont autant d'instructions de recherche de preuve.
On discutera ensuite de la possibilité d'utiliser ce cadre pour
formuler
dans les termes
interactifs de la Ludique des mécanismes de contrôle de la
recherche comme
le
backtracking ou la coupure qu'il est difficile de modéliser
logiquement dans
l'approche
traditionnelle (ii).
Mardi 21 avril 2009
10.30 Benoit Razet, INRIA Rocquencourt
Calculs non-déterministes relationnels avec des machines
d'Eilenberg.
Les machines d'Eilenberg sont un modèle de calcul
non-déterministe à
base de relations qui repose sur les automates finis de la
théorie des
langages formels. Samuel Eilenberg introduisit ce modèle en 1974
parce
qu'il rend compte des principaux dispositifs calculatoires de la
théorie des automates tels que les automates finis, les
transducteurs,
les automates à piles mais aussi les machines de Turing. Une
machine
d'Eilenberg est un automate étiqueté par des relations
binaires
d'un ensemble quelconque. En interprétant la
concaténation sur les mots
par la composition sur les relations, une machine d'Eilenberg
définit
une union de compositions de relations. Les relations étant
fermées par
union on dit du modèle qu'il est modulaire. Le
non-déterminisme apparaît
à deux niveaux pour une machine : celui du graphe (décrit
par un
automate non-déterministe) et celui des relations
(modélisant une
opération non-déterministe).
Nous proposons une méthode pour simuler les machines d'Eilenberg
en
utilisant un moteur réactif manipulant des flux. Nous
détaillerons
cette approche sur les machines d'Eilenberg finies pour lesquelles la
formalisation a été complètement effectuée
avec l'assistant de preuves
Coq. Ensuite nous indiquerons comment étendre ce travail pour
des
machines d'Eilenberg conduisant à un paradigme très
général de
programmation relationnelle.
Mardi 17 mars 2009
14.30 Nacim RAMDANI, INRIA Coprin
Non-linear continuous reachability
analysis using interval
constraint programming
Hybrid systems are complex dynamical systems which involve the
interaction of discrete and continuous dynamics, and are often
components of safety-critical systems. Hence, computing reachable sets
for hybrid systems is an important step when one addresses verification
or synthesis tasks. A key issue then lays in the calculation of the
reachable set for continuous dynamics with nonlinear models, even more
when uncertainty is present.
In this talk, I will show how to compute an overapproximation for the
reachable set of uncertain nonlinear continuous dynamical systems by
using guaranteed set integration. I will introduce several ways to do
so.
The first way relies on a full interval method which handles whole
domains for set computation and relies on state-of-the-art validated
numerical integration methods, via Taylor series and interval analysis.
I will introduce both techniques, and give illustrative examples
using
Nedialkov VNODE software.
The second way can be used with monotone systems only but makes it
possible to bracket the uncertain nonlinear system between two
nonlinear
dynamical systems where there is no uncertainty. I will overview
monotone systems and show how to use comparison principles for such
systems for computing reachable sets.
A third way relies on the Muller's existence theorem for differential
inequalities in order to bracket any uncertain dynamics between two
dynamical systems where there is no uncertainty. Here again, I will
recall this theorem and show how to use it for computing reachable
sets.
For the second and third ways, the obtained bracketing systems, which
may be coupled, are often piecewise Ck-differentiable functions. Then,
validated numerical integration methods cannot be used directly. Hence,
our contribution resides in the use of hybrid automata to model the
bounding systems. I give a rule for building these automata and show
how
to run them and address mode switching in a guaranteed way in order to
compute the over approximation for the reachable set. Here we also make
use of solving methods for numerical constraint satisfaction problems.
The computational cost of our method is also analyzed and shown to be
smaller that the one of classical interval techniques. Sufficient
conditions are given which ensure the practical stability of the
enclosures given by our hybrid bounding method. Examples are given
which
show that the performance of our method is very promising.
Mercredi 11 mars 2009
11.15 Claudine Chaouiya, Instituto
Gulbenkian de Ciência - Oeiras, Portugal
Qualitative Modelling of regulatory
networks using High Level Petri nets: application to developmental
processes
Great advances in molecular biology, genomics and functional genomics
open the way to the delineation of regulatory maps controlling
essential biological processes. To assess the behaviours induced by
these large and complex networks, dedicated mathematical and
computational tools are very much required. Here, we focus on pattern
formation that relies on intracellular and intercellular interactions.
We will briefly present two applications, which motivate our work, both
related to Drosophila development. The first case deals with the
regulatory processes underlying the dorsal appendage morphogenesis in
the Drosophila egg. The segment-polarity module involved in the
segmentation of the Drosophila embryo constitutes our second example.
We rely on the logical formalism to model and analyse the
qualitative behaviours of the regulatory networks. After a short
presentation of the logical framework, we will show how such models can
be represented by means of High Level Petri nets. This representation
allows us to define compact models for regulatory modules (here, a
module will constitute an intracellular network) and then to compose
modules interacting through intercellular signals following a given
neighbouring relation. At this stage, we provide a convenient way to
settle models defined as the composition of modules that are crucial in
patterning processes. Finally, implementation aspects will be
discussed.
Joint work with Franck
Pommereau (LACL, Université Paris
12) and Hanna Klaudel (IBISC Université d'Evry-Val d'Essonne)
Mercredi 11 mars 2009
10.30 Aurélien Naldi, TAGC,
Univ. de Marseille
A Reduction of logical regulatory graphs preserving essential dynamical properties
As ever larger biological molecular regulatory networks are
delineated, standard dynamical modelling and analysis approaches are
reaching their limits. To cope with the increasing complexity of these
networks, we have defined a reduction method for multi-valued logical
models. Starting with a detailed model, this method enables the
computation of a reduced model by iteratively "hiding" regulatory
components. To keep a consistent behaviour, the regulators of the
hidden nodes become regulators of their targets, for which new logical
functions are determined.
The construction of reduced models ensures the preservation of a
number of dynamical properties of the original model. In particular,
stable states and more complex attractors are conserved. More
generally, we address the question of the relationship between the
attractor configuration of the original model and that of the reduced
model, along with the issue of attractor reachability.
This novel reduction method has been implemented into our software
GINsim, and will be illustrated through its application to model
of networks involved in the control of helper T lymphocytes differentiation.
Joint work
with E. Remy, D. Thieffry, C.
Chaouiya
Vendredi 6 mars 2009
10.30 Fabien Corblin, IMAG Grenoble
Conception et mise en oeuvre d'un
outil déclaratif pour l'analyse des réseaux
génétiques discrets
Une demande croissante d'outils pour construire et décrypter des
réseaux génétiques contrôlant des processus
cellulaires est ressentie
en biologie. Nous soutenons que l'utilisation de l'a'pproche
déclarative
est pertinente et applicable pour répondre aux questions des
biologistes sur ces réseaux, en général
partiellement connus. L'idée
principale est de modéliser des connaissances portant à
la fois sur la
structure et la dynamique d'un réseau par un ensemble de
contraintes
représentant l'ensemble des solutions, de vérifier sa
cohérence, de
réparer une incohérence éventuelle par un
relâchement automatique, et
d?inférer des propriétés sur la structure et la
dynamique du réseau.
Pour montrer la faisabilité de l'approche, nous formalisons les
réseaux
discrets de R. Thomas et les propriétés biologiques
pertinentes,
proposons un outil reposant sur la programmation logique par
contraintes en coopération avec un solveur SAT, et la validons
sur des
applications biologiques significatives.
14.00 Benjamin Pfeuty, ERATO Complex Systems
Biology, University of TokyoFabien Corblin, IMAG Grenoble
Modeling G1 phase of
mammalian cell cycle: cell fate determination and cancer onset
Upon their exit from mitosis, mammalian cells enter a G1 phase during
which they acutely sense all sorts of environmental stimuli. On the basis
of these signals that they first need to decipher and integrate, they
decide whether to undergo division, quiescence, differentiation, senescence
or apoptosis. Failures in this process may lead to cancer.
In this study, I questioned whether, despite the complexity of the G1
regulatory network, simple organizing principles might be identified that
could explain how specific input signals are converted into appropriate
cell fates. For this purpose, a mathematical model of the G1 regulatory
network has been formulated using a simplified description of activities
linked to signal transduction, cell growth, cell division and cell death.
Bifurcation analysis of the model revealed the existence of multistability
between several attractor states corresponding to G0 -arrest, G1 -arrest,
S-phase entry and apoptosis cell fates.
I will discuss the result of this modeling study from different
perspectives: (i) from a modeler's perspective, how to design a model that
captures the qualitative behavior of a certain biological process or
system; (ii) from an engineer's perspective, how feedback and feedforward
loops are combined within a regulatory network to drive the
signal-dependent switch between distinct cellular processes; (iii) from a
biologist's perspective, how the control of cell fate determination have
evolved in multicellular organisms and how it could fail thereby enabling
the emergence of cancers.
Mardi 13 mai 2008
10.30 Hugues Berry, INRIA Saclay
Individual-based simulations for cell
biochemistry in crowded environments
Standard modeling works in cell biochemistry are usually based on
mean-field equations, most often referred to as "laws of mass-action".
Yet, the derivation of these laws is based on strict assumptions. In
particular, the reaction medium must be dilute, perfectly-mixed,
three-dimensional and spatially homogeneous and the resulting kinetics
are purely deterministic. Many of these assumptions may be violated in
cells. Notably, single-cell measurements show that protein diffusion in
most compartments (including cytosol, nucleus and membranes) is
subdiffusive (anomalous diffusion). This phenomenon is mainly caused by
physical obstruction to diffusion due to large-size obstacles, that
actually abound in cells (organelles, internal networks, large
macromolecular complexes...). Fundamentally, this experimental
observation tells us that diffusion in cells is not perfectly mixing
and that cellular media can be considered as spatially inhomogeneous.
My objective is thus to try and evaluate what kind of behaviors can be
expected that are not accounted for by the laws of mass-action.
To simulate these effects, usual stochastic kinetic approaches such as
Gillespie's algorithms are not well suited, because they explicitly
assume perfect mixing and do not take into account physical
obstruction. Conversely, lattice gas automata or individual-based
modeling appears to be the most appropriate tools.
I will present a first example concerning simple enzyme reactions in
cell membranes with molecular crowding. Individual-based simulations
indicate that the classical mean-field formalism for these reactions
(Michaelis-Menten kinetics) fails short of describing the kinetics.
Conversely, so-called "fractal" kinetics can be used to describe the
observed behaviors. Furthermore, the simulations uncover a spontaneous
tendency to segregate reaction substrates and products within distinct
spatial zones of the membrane, i.e. a phenomenon similar to
morphogenesis. Finally, I will present current perspectives &
ongoing works concerning modeling of aging and protein aggregation in
E. coli (with F. Taddei and A. Lindner, U571 INSERM, Necker,
Paris) and the development of hybrid discrete/continuous
simulation methods
Joint workwith Olivier Michel, Ibisc Lab., University of Evry, Genopole
and A. Lesne, IHES, Bures-sur-Yvette and LPTMC, Univ. P & M. Curie,
Paris, France.
Vendredi 15 février 2008
11.00 Antoine Spicher, LORIA
Spatial Programming of an Amorphous
Biological Medium
The MGS project is aimed at studying the use of topological notions for
programming languages and their applications in developing new data and
control structures for the simulation of dynamical systems with a
dynamical structure. These goals have led, at a theoretical level,
to the development of an approach based on two new concepts:
1. the topological collections, a new kind of data
structure relying
on the notion of cellular complex developed in algebraic topology, and
2. the transformations, an original kind of case-based
definition of
functions on topological collections
These concepts are implemented in an experimental programming language
dedicated to the specification of dynamical systems: the MGS language.
My thesis work is organized following three directions:
1. developing the notion of topological collection of
arbitrary
dimension
2. specifying a formal semantics for MGS, especially for
transformations, and finally
3. validating these works with numerous non trivial
examples in
biology and morphogenesis.
These applications are mostly examples of dynamical systems with a
dynamical structure: the simulation of the cellular motility by
adaptive mesh subdivision, the modeling of the neurulation that
exhibits
a topological modification, the numerical exact stochastic simulation
of
chemical models, the modeling of plant growth coupling hormones
diffusion and cellular differentiation, declaratives implementations
of complex CAD operations like mesh refinement...
During the presentation I will start with an overview of these works.
Then I will focus on a particular example where a specific rule
application strategy based on the Gillespie stochastic simulation
algorithm is used to model chemical reactions. Finally I will present a
perspective that consists in developing a formalism to specify and
analyze a global spatial behavior and to compile it in the local
behaviors of entities of a population and to take advantage
of
emerging properties. This project relies on recent results in different
domains like spatial programming, amorphous computing and synthetic
biology.
Lundi 11 février 2008
10.30 Jean Krivine, LIX, Palaiseau
Une plateforme pour la
simulation et l'analyse de systèmes bio-moléculaires en
k-calcul
Travaux réalisés en collaboration avec Vincent Danos
(Laboratoire
Preuves Programmes et
Systèmes, CNRS), Jerome Feret (Ecole Normale Supérieure,
Paris), Walter Fontana (Systems Biology Department, Harvard Medical
School, US).
Dans cet exposé nous présenterons une plateforme en cours
de
dévoloppement à Plectix Biosystems (Cambridge US)
permettant
d'analyser et de simuler de larges systèmes
bio-moléculaires décrits
dans le k-calcul de Danos et Laneve [1].
Nous introduirons en premier lieu les concepts de base de la
modélisation dans le k-calcul [2], puis nous présenterons
ensuite un
algorithme de simulation permettant de produire des executions
stochastiques d'un système k avec un coup par
événement de calcul
(application d'une règle et mise à jour du
système) constant et
indépendant du nombre d'agents simulés [3].
[1] Formal Molecular Biology, Danos et Laneve. TCS 325, 2004
[2] Rule-based modelling of cellular signalling, Vincent Danos, Jerome
Feret, Walter Fontana, Russell Harmer, Jean Krivine. CONCUR'07.
[3] Scalable simulation of cellular signaling networks, Vincent Danos,
Jerome Feret, Walter Fontana, Jean Krivine. APLAS'07.
Vendredi 25 janvier 2008
10.00 Jacques-Alexandre
Sepulchre, INLN CNRS, Nice
Effets de rétroaction dans les
cascades de signalisation intracellulaire
Classiquement, une voie de signalisation consiste en une cascade de
réactions enzymatiques élémentaires
où, à chaque étape, une protéine
est activée par une modification covalente induite par la
réaction
précédente. De plus, une fois activée, cette
protéine peut jouer le
rôle d'enzyme pour la réaction suivante.
Dans ce contexte, l'exemple
le plus connu de modification covalente est le processus de
phosphorylation/déphosporylation dans lequel la protéine
est
généralement activée par l'ajout d'un groupe
phosphate et désactivée
par son retrait.
Un exemple connu dans ce contexte est celui des cascades de MAPKs
(Mitogen Activated Protein Kinases). Partant d'une
description
complète d'une cascade de cycles
élémentaires, décrite en termes de
loi d'action des masses, nous avons dérivé une
approximation
rigoureuse des équations cinétiques de la chaîne
dans laquelle chaque
cycle est décrit par une seule variable. Le système
d'équations que
nous obtenons est différent de celui qui est utilisé
depuis plusieurs
années dans la littérature, lequel est une extension
purement
phénoménologique du modèle de
Goldbeter-Koshland. Notre approche met
en évidence certaines nouvelles propriétés qui,
bien qu'implicitement
contenues dans le modèle complet, étaient absentes dans
l'approximation
phénoménologique. Une propriété
clé qui apparaît dans notre jeu
d'équations est l'existence d'une rétroaction
exercée par chaque cycle
de la chaîne sur son prédécesseur.
Cette rétroaction est non
seulement à l'origine d'oscillations temporelles amorties
prédites par
le modèle, mais aussi montre qu'un signal biochimique peut
se
propager pas seulement en aval dans la chaîne,
mais aussi en amont.
Cette propriété, qui se retrouve dans le
système complet, remet en
question l'idée implicite qu'une voie de signalisation est
unidirectionnelle.
Jeudi 4 octobre 2007
10.30 Carlos Orlate and Frank
Valencia, LIX Ecole Polytechnique
A Process Calculus for Universal
Concurrent Constraint Programming: Semantics, Logic and Application
We introduce the Universal Timed Concurrent Constraint Programming
(utcc) process calculus; a generalisation of Timed Concurrent
Constraint Programming. The utcc calculus allows for the
specification
of mobile behaviours in the sense of Milner's pi-calculus: Generation
and communication of private links. We first endow utcc with an
operational semantics and then with a symbolic semantics to
deal with
problematic operational aspects involving infinitely many substitutions
and divergent internal computations. The novelty of the symbolic
semantics is to use temporal constraints to represent finitely
infinitely-many substitutions. We also show that utcc has a
strong
connection with Pnueli's Temporal Logic. This connection can be used to
prove reachability properties of utcc processes. As a compelling
example, we use utcc to exhibit the secrecy flaw of the
Needham-Schroeder security protocol.
Mardi 31 juillet 2007
14.00 Ludovic Langevine, Mission
Critical, Belgium
Ontology Driven Software Engineering
for Real Life Applications
In development of any large scale software systems the Business has a
vision for a project to transform the company. However the vision is
informally and incompletely specified and subject to frequent changes
that leads to the Business-IT gap. This gap makes it difficult for IT
to give a reasonable estimate of time and cost for the project and
impacts greatly on the business case. Our experience shows that the
gap can be bridged by describing the business knowledge in a formal
language understandable by Business and consumable by computer
programs.
The Web Ontology Language, OWL, was developed to facilitate greater
machine interpretability of human knowledge by providing additional
vocabulary along with formal semantics. OWL ontologies can be enriched
by business rules using the Semantic Web Rule Language, SWRL. Those
languages forms a knowledge continuum between Business and IT, and
provides a mechanism by which the Business can drive the evolution of
the project by proposing concrete changes to the ontology.
In this talk, we will describe the ODASE platform (Ontology Driven
Architecture for Software Engineering) and demonstrate some
pedagogical applications. We will show how automatic code generation,
on top of a formal description of the Business domain, bridges the
Business-IT gap, increases the quality and the flexibility of the
application, and reduces its development and maintenance cost.
Mardi 17 juillet 2007
10h00 Jacques Robin, University of
Recife, Brazil.
Towards CHR components: preliminary
ideas on implementing adaptive
solvers for the built-ins constraints
of a CHR base, as another CHR base
CHR was conceived as a host programming platform extension with
constraint solving rules. Any CHR base is thus a client of such host
platform that it uses as a server to solve the so-called built-in
constraints which solving is needed by the CHR base but for which there
are
no definition in that base (i.e., these constraints appear only in rule
guards and bodies of the CHR base but not in any rule head). This
single
client-server relationship between a CHR base and a host programming
platform can be generalized into N client-server relationships in a
component assembly of CHR bases. In such an assembly the constraints
that
appear only in the guards and bodies of a client component CHR base,
appear
in the heads of its server component CHR bases. We suggest some simple
methods for the server CHR base to be used to check the rule guard
entailment conditions of its client CHR bases. These methods could
serve as
the basis to extend CHR with software components, to allow low-cost
engineering of large-scale and partially reusable CHR applications.
Mardi 10 juillet 2007
10h00 Jacques Robin, University of
Recife, Brazil.
CHROME: a Component-Based Aspect and
Object Oriented Model-Driven
Architecture for a CHRv Engine
CHROME is an ongoing effort to integrate cutting-edge
reuse-fostering software engineering techniques such as components,
aspects,
and object-oriented model transformations and apply them to the
development
of an easily reusable and extendable adaptive inference engine for the
knowledge representation language Constraint Handling Rules with
Disjunctive
bodies (CHRv). Following model-driven engineering a fully refined
platform
independent model of the engine is first specified in UML2 and then
automatically transformed in several steps into source code of
mainstream
component-based object-oriented imperative platforms such as Java OSGi
or
C#.Net by way of model transformations implemented in INRIA's Atlas
Transformation Language. By leveraging the high expressivity and
versatily
of CHRv, CHROME aims to constitute the base building block of a
component
framework offering in an integrated way a variety of automated
reasoning
services such as deductive entailment and
satisfiability, individual classification and concept subsumption,
various
forms inheritance, default reasoning, abductive explanation generation,
truth maintenance, belief revision, belief update, temporal
projection,
planning and constraint solving in any domain.
Jeudi 5 avril 2007
13h30
Samuel Bernard, Humboldt University, Berlin, Germany.
Synchronization-Induced Rhythmicity of Circadian Oscillators in the Suprachiasmatic Nucleus
The suprachiasmatic nuclei (SCN) host a robust,
self-sustained circadian
pacemaker that coordinates physiological rhythms with the daily
changes in the environment. Neuronal clocks within the SCN form a
heterogeneous network that must synchronize to maintain timekeeping
activity. Coherent circadian output of the SCN tissue is established
by intercellular signaling factors, such as vasointestinal
polypeptide (VIP). It was recently shown that besides coordinating
cells, the synchronization factors play a crucial role in the
sustenance of intrinsic cellular rhythmicity. Disruption of
intercellular signalling abolishes sustained rhythmicity in a
majority of neurons and desynchronizes the remaining rhythmic
neurons. Based on these observations, we propose a model for the
synchronization of circadian oscillators that combines intracellular
and intercellular dynamics at the single-cell level. The model is a
heterogeneous network of circadian neuronal
oscillators where individual oscillators are damped rather
than self-sustained. We simulated different experimental conditions and found that:
(i) In normal, constant conditions, coupled
circadianoscillators quickly synchronize and produce a coherent output.
(ii) In large
populations, such oscillators either synchronize or gradually lose
rhythmicity, but do not run out of phase, demonstrating that rhythmicity and synchrony are
co-dependent.
(iii) The number of oscillators and connectivity are important for
these synchronization properties.
(iv) Slow oscillators have a higher impact on the period in mixed
populations.
(v) Coupled circadian oscillators can be efficiently entrained by
light-dark cycles.
Based on these results, we predict that:
(i) SCN neurons need periodic synchronization signal to be rhythmic.
(ii) A small number of neurons or a low connectivity results in
desynchrony.
(iii) Amplitudes and phases of neurons are negatively correlated.
We conclude that to understand the orchestration of timekeeping in the
SCN,
intracellular circadian clocks cannot be isolated from their
intercellular communication
Mercredi 4 avril 2007
10h30 David Angeli, University of
Firenze, Italy & INRIA Rocquencourt
Structural monotonicity of chemical reaction networks
Systems biology is a cross-disciplinary field which aims at
understanding cell life at the molecular
level, viz. by systematically understanding and identifying the
complex chemical interactions that take
place within individual cells and between neighboring ones. From the
point of view of a systems scientist
this poses remarkable challenges both for modeling and qualitative
understanding of the possible dynamical behaviours
which such models may exhibit. In this talk we try to analyze the
dynamical behaviours of chemical reaction
networks by taking into account the huge uncertainties that such models
often entail. We seek for qualitative
criteria which may apply to ODE models regardless of specific
parameters values and which still can provide useful tools for
the study of their dynamics. Technical tools used range from
monotonicity theory, to Petri nets and graph theory.
Biography:
David Angeli graduated in 1996 from University of Florence in Control Engineering, and later obtained his phD degree in Automation within the Dep. of Systems and Computer Science from the same university.
He is currently an Associate Professor in Florence as well as a visiting fellow of INRIA de Rocquencourt, Paris. His research interest include nonlinear stability analysis, chemical reaction networks, monotone dynamical systems.
Mercredi 14 mars 2007
10h30 Monika Heiner, Cottbus Technical
University, Germany & INRIA Rocquencourt
Modelling and Analysis of Biochemical Networks - a Petri Net
Perspective on Systems Biology
Petri nets are well-known for an intuitive and executable modelling
style, supporting at the same time exhaustive analysis techniques.
Their
success stories cover application areas in various engineering
disciplines, where they have been proven to be useful for the sound
construction of technical systems. In this talk we bridge the gap from
the technical systems to natural systems and demonstrate how
well-established techniques can be reused for (some of the) challenges
current systems biology is confronted with. No prerequisite knowledge
is
assumed.
Mardi 9 janvier 2007
11h00 Grégory Batt, Boston
University
Combining discrete abstraction and model checking for the analysis of partially-known models of natural and synthetic gene networks
Natural gene networks are complex networks of interregulating genes that control at the molecular level the development and functioning of living organisms. Synthetic gene networks are engineered networks that confer a desired behavior to a living organism. Understanding the functioning of these networks is a central problem in systems biology and in bioengineering. However, their complex dynamics, due to the presence of feedback loops and non-linear phenomena, often defeats intuitive understanding. Moreover, the lack of precise information on parameter values hampers a model-based analysis or design of these systems.
In this talk, I will present two recently-developed methods for the verification of the dynamical properties of gene networks under parameter uncertainty. Both methods combine discrete abstraction and model checking. Discrete abstraction is used to obtain a discrete representation of the dynamics of the system in the state space for sets of parameters, and model checking is used for the verification of the dynamical properties of the abstract, discrete system. The approximations obtained by discrete abstraction are conservative. This guarantees that the properties satisfied by the abstract system also hold for the original one.
The above strategy is applied to the analysis of two different types of models, namely piecewise affine and piecewise multiaffine differential equation models. Both types of models capture essential features of genetic regulations but with different levels of detail. A coarse-grained, qualitative approach is used for the analysis of piecewise affine models. This method is well-adapted to the essentially qualitative information available on natural gene networks. A finer-grained, quantitative approach is used for the analysis of piecewise multiaffine models, well-adapted to the better-known synthetic gene networks. Though quantitative, this approach can deal with uncertain parameters specified by intervals.
The practical applicability and biological relevance of the proposed approaches are illustrated by means of two examples: the validation of a model of the nutritional stress response and the tuning of a synthetic transcriptional cascade, both in the bacterium E. coli.
Work done in collaboration with:
- Hidde de Jong (INRIA), Johannes Geiselmann (UJF, Grenoble), Jean-Luc Gouzé (INRIA), Radu Mateescu (INRIA), Michel Page (UPMF, Grenoble), Delphine Ropers (INRIA), Tewfik Sari (UHA, Mulhouse) and Dominique Schneider (UJF, Grenoble)
and
- Calin Belta (Boston University), Boyan Yordanov (Boston University) and Ron Weiss (Princeton University)
Jeudi 14 décembre 2006
11h00 Khalil Djelloul,
Université d'Ulm, Allemagne
CHR et les contraintes du premier ordre autour des arbres
CHR (Constraint Handling Rules) est un langage de programmation
logique à base de règles de réécriture
créé par Thom Fruehwirth dans les années 1990 et
dont le fonctionnement est régit par une
sémantique raffinée. Un des premiers solveurs CHR
publiés est le fameux "CHR-Term-Unification-Algorithm"
présenté par Thom
Fruehwirth en 1993 et révisé en 1998. Ce solveur
élégant sous
forme de 4 règles de réécriture permet de
résoudre des conjonctions d'équations à
termes éventuellement non-plats (termes contenant plusieurs
symboles de fonction
imbriqués) dans l'algèbre des arbres rationnels. Il
a
également un intérêt indéniable en
programmation car il effectue l'unification des
termes : le coeur même de Prolog et de plusieurs autres langages
de
programmation logique. Cependant, ce dernier utilise un ordre
"<" sur les
termes et les variables, et sa complexité est une conjecture qui
dure
depuis plus de 10 ans.
Nous montrons dans cet exposé que ce solveur est de complexité exponentielle (en temps et espace) quelque soit l'ordre "<" choisi et déduisons de cette preuve une complexité quadratique O(n2) dans le cas où les termes des équations contiennent au plus un seul symbole de fonction. Nous étendons ensuite ce solveur par quelque règles CHR afin que ce dernier puisse résoudre, en une complexité quadratique, toute conjonction quantifiée d'équations à termes non-plats dans la théorie des arbres finis ou infinis. Nous terminons cet exposé en présentant une implantation CHR d'un solveur de contraintes du premier ordre dans une théorie étendue "T" d'arbres finis ou infinis, donnant des solutions claires et explicites aux problèmes de satisfaction de contraintes du premier ordre dans "T". Pour cela, nous étendons d'abord la signature et l'axiomatisation de Maher (1988) de la théorie des arbres finis ou infinis par une relation fini(x) qui contraint le terme "x" à être un arbre fini. Nous présentons ensuite notre solveur CHR et montrons entre autres comment modéliser et résoudre une contrainte du premier ordre dans "T" par des règles CHR. Enfin, nous comparons les performances de notre solveur CHR avec ceux obtenues en utilisant une implantation C++ de ce solveur et de notre récente procédure de décision dédiée aux théories décomposables.
Mercredi 25 octobre 2006
11h00 Andras Kovacs, Post Doc ERCIM
Capacitated lot-sizing with sequence-dependent setups
In this talk, I will give a brief review of different models of the
lot-sizing and scheduling problem, and introduce our novel results on
modelling the common practical requirement of sequence-dependent setups.
Although lot-sizing problems have been studied in Operations Research for
many years, the latter requirement still presents a challenge for current
optimization techniques.
I will present a novel MIP formulation of the single-machine capacitated
lot-sizing and scheduling problem with sequence-dependent setup times and
setup costs. The model is based on determining during pre-processing all
item sequences that can appear in given time periods in optimal solutions.
The sequences are used in a mixed-integer program, parameters of which are
generated by a heuristic procedure in order to establish a tight
formulation. This model allows us to solve significantly larger problems
than what was tractable by earlier optimal solution methods, and it often
achieves orders of magnitude speedup.
Vendredi 6 octobre 2006 (salle de
conf. Bât. 11)
11h00 Jacques Robin, Universidade
Federal de Pernambuco, Brazil.
Towards a Model-Driven Automated Reasoning Component Framework Based on
Constraint Handling Rules.
Over the last two decades automated reasoning techniques have
tremendously
diversified while becoming far better understood, formally founded and
scalable. They nevertheless remain highly underused in the larger than
ever
number of mainstream software services to which they could bring a
decisive
competitive edge. This is mostly due to the fact that the high level of
conceptual reuse existing among these techniques, has not been
leveraged in
the software architectures of available automated reasoning systems,
making
them overly difficult and costly to use, reuse, extend, customize and
integrate in larger systems. The on-going ORCAS project, a cooperation
involving several research groups, addresses this issue. It integrates
four
model-driven software reuse approaches (task model reformulation,
component
model assembly, aspect model weaving, and code generation) to develop a
framework of reusable automated reasoning components. It leverages and
integrates UML2 and related OMG standards for high-level
modeling, Constraint Handling Rules (CHR) for formal knowlege
representation
and Java for executable code deployment.
Mercredi 22 février 2006
14h00
K.
Sriram,
Epigénomique,
Génopole Evry,
I. Delay model for mammalian
circadian rhythms and
II. Mathematical model on the dynamics of cyclical organization of
simple protein network and its application to budding yeast cell cycle.
The talk consists of two parts in which discrete delay model for
mammalian circadian rhythms will be dealt with in the rst part
and in the second part dynamical analysis of cyclical organization of
protein networks and its application to cell division cycle will be
presented. A brief abstract is given below.
Part I: A three variable discrete delay model is proposed for the
circadian rhythm of the mammals with BMAL1, PER-CRY complex and
REV-ERB® protein concentrations as the dynamical variables. The
delay model is phenomenological in nature rather than the precise
description of all the underlying complex processes. The goal is to
study the e ects of delay in the circadian rhythms of mammals that
appears in both the positive and negative feedback loops of the model.
The delay model exhibits 24 hr limit cycle oscillations, entrainment to
Light-Dark (LD) cycles and phase response curves. The model is also
found to exhibit quasiperiodic and chaotic oscillations under LD cycles
when delay is varied. These are linked to non 24 hrs sleep wake
syndrome and cancer incidence. The delay model in essence, captures the
core mechanism of the mammalian circadian rhythms with a fewer number
of variables and parameters.
Part II: The dynamics of the cyclical organization of simple protein
networks and its application to the budding yeast cell cycle are
studied by constructing nonlinear models. The protein network consists
of two small cyclical loops, where each loop in the absence of
interaction with the other exhibit di erent dynam- ical behavior.
Bistability is exhibited by one loop and limit cycle oscillations are
exhibited by the second loop. Coupling of both the cyclical loops by
positive feedback loop displays complex behavior such as multi-
stability and coexistence of limit cycle and multiple steady states.
The coupling of two cyclical loops by the positive feedback loop brings
in the notion of checkpoint in the model. The model also exhibits
dominoe like behavior, where limit cycle oscillations takes place in a
stepwise fashion. As an application, the events that govern the cell
cycle of budding yeast is considered for the present study. In budding
yeast, the feedback interactions among the important transcription
factors, cyclins and its inhibitors in G1, S-G2 and M phases are
considered for the construction of the biological circuit diagram.
Surprisingly, the sequential activation of the transcription factors,
cyclins and its inhibitors forms two independent cyclical loops, with
transcription factors involves in the cyclic positive regulation in
clockwise direction, while the cyclins and its inhibitors involves in
the negative regulation in anticlockwise direction. The coupling of the
transcription factors and the cyclin and its inhibitors by positive
feedback loops generates rich bifurcation diagram that can be related
to the di erent events in the G1, S-G2 and M phases in terms of
dynamical system theory. The different checkpoints in the cell cycle is
accounted for by appropriately silencing the positive feedback loops
that couples the transcription factors and the cyclin and its
inhibitors.
Mercredi 8 février 2006
14h00 Eric Reiter, INRA Tours
Mécanismes de
signalisation cellulaire induits par les récepteurs
couplés aux protéines G:
exemple du récepteur de l'hormone folliculo-
stimulante (FSH).
Les récepteurs couplés aux protéines G (GPCR)
représentent de loin
la famille de récepteurs membranaires la plus abondante et la
plus
versatile chez les mammifères. Des GPCRs sont cruciaux pour
l'ensemble
des grandes fonctions physiologiques: perception sensorielle (vision,
odorat, nociception,...), neurotransmission, systèmes
endocriniens,
.. etc. Pour cette raison, les GPCRs sont directement ciblés par
plus de la moitié des médicaments actuellement
utilisés. Comprendre
les mécanismes généraux et particuliers qui
régissent la signalisation
cellulaires de ces récepteurs ou de certains d'entre eux reste
une
question centrale en biologie.
Seulement trois familles de protéines sont capables de
reconnaître
et d'interagir spécifiquement avec les GPCRs après qu'ils
aient été
activés par leur ligand: les protéines G
hétérotrimériques, les kinases
des GPCRs (GRKs) et les b-arrestines. Au cours des 30 dernières
années,
les concepts concernant la transduction des GPCRs et leur pharmacologie
ont découlés du rôle joué par les seules
protéines G hétérotrimériques.
Au cours de la première partie de ce séminaire, je
traiterais des
fonctions signalétiques nouvelles des GRKs et des b-arrestines.
Je comparerais les contributions respectives des voies protéine
G
et b-arrestines dependantes dans l'activation des MAP kinases ERK
par différents GPCRs; le rôle modulateur des GRKs ainsi
que les sensibilités
respectives des deux mécanismes d'activation des ERKs.
Dans une seconde partie, j'expliquerais plus particulièrement
notre
problématique de recherche sur le récepteur de la FSH
ainsi que les
grandes lignes du projet de signalisation à « haut
débit » que nous
voulons mettre en place.
Vendredi 3 février 2006
10h30 Francis Lévi, INSERM
Villejuif,
Implications thérapeutiques des
interactions entre cycle cellulaire et rythme circadien en cancérologie
Jeudi 26 janvier 2006 (salle de
conférence du bâtiment 11)
10h30 Nicolas Beldiceanu, Ecole des
Mines de Nantes,
Graph-Based Filtering
Joint work with : M. Carlsson, T. Petit, J.-X. Rampon, G. Rochart, C.
Truchet
Over the past 20 years global (combinatorial) constraints have gradually
been introduced within the area of constraint programming for dealing
with concrete problems.
Efficient filtering algorithms, usually based on graph theory, were
developped in an ad-hoc
way for each global constraint.
This talk presents a systematic approach which aims at providing
generic filtering
algorithms for global constraints. Given a specification of a global
constraint C in terms
of graph properties, we show how to derive a filtering algorithm for C
(i.e., check feasibility
and eliminate infeasible choices). For this purpose we present three
complementary methods:
(1) The first method is based on the bounds of the graph properties
used in the
description of a global constraint. We provide lower and upper bounds
for frequently
used graph properties (number of arcs, vertices, connected components,
strongly
connected components, sinks).
(2) The second method shows how to determine the status of vertices and
arcs of an
intermediate digraph so that the final digraph does not contain more
than
(resp. does no contain less than) a given fixed number of arcs,
vertices, connected
components, strongly connected components, or sinks.
(3) The third method presents a database of about 200 graph invariants
for deriving
systematically necessary conditions when a global constraint is defined
by more than
on graph property.
We conclude with different questions raised by this approach.
14h00 Nicolas Beldiceanu, Ecole des
Mines de Nantes,
Contraintes d'arbres et applications
aux problèmes de
phylogénie et aux problèmes de cheminement
Travail fait avec: Xavier Lorca, Pierre Flener, Irit Katriel
La première partie dresse un apercu général sur les contraintes de couverture
de graphe par des arbres, à la fois dans le cas de graphes orientés et le cas
de graphes non-orienté. Nous présentons trois contraintes de couverture par des
arbres et nous montrons comment assurer la consistance hybride (hybride car on
utilise à la fois des variables ensemblistes et des variables domaines) pour ces
trois contraintes.
La deuxième partie se focalise dans le cadre de graphe orientés sur la prise
en compte de contraintes additionelles (contraintes de précédences,
d'incomparabilité, de degré maximum) rencontrées dans des applications pratiques.
Elle donne les résultats obtenus sur des problèmes de phylogénie et de cheminement.
Lundi 23 et mardi 24 janvier 2006 (Institut Henri
Poincaré, Paris)
Abstraction,
modularité et compositionalité dans les réseaux
géniques et protéiques
Réunion de l'ACI VicAnne et réunion de lancement
de l'ARC MOCA
Mercredi 11 janvier 2006:
14h00 Stephanie
Spranger, Ludwig Maximilian University, Munich, Germany,
Calendars as Types
Data Modelling, Constraint Reasoning, and Type Checking with Calendars
I have investigated real-life calendars, calendar and time
expressions, and time and date formats. This work aims at the
development of computer-based tools for modeling and processing such
calendric data. The realization is based on a programming language
approach to time and calendars that essentially differs from
logic-based and algebraic approaches. The thesis underlying this work
is twofold: (1) "Calendar as Type", i.e. time and calendar
expressions are not modeled in a logic or an algebra but instead, by
means of data types. The user is provided with a set of language
constructs (so-called type constructors). Advantages of this approach
are: user-friendly modeling, increase of efficiency and consistency,
program and document annotation, and abstraction. (2) "Theory
Reasoning", i.e. problems such as appointment scheduling or travel
planning are formulated in the environment of a constraint solver
specific to arbitrary calendar domains (i.e.user-defined data types
like "day'' or "consultation hour'') rather than by axiomatization,
commonly used with approaches based on ontology modeling and
reasoning. The constraint solver refers to and relies on
(user-defined) calendric types, it maintains the semantics of
different calendric types like "day'' and "consultation hour'', and
it allows for efficient constraint solving with arbitrary calendric
data.
This work shows perspectives for future research on using data types
and specific inference algorithms (e.g. constraint solving) for
modeling and reasoning on specific theories (e.g. topologies and
locational data).
The calendar modeling language CaTTS is an outcome of this work.
This talk introduces into CaTTS and its Multi-Calendar constraint solver.
Lundi 19 décembre 2005:
14h00 Khalil Djelloul,
Université de Marseille Luminy,
Théories complètes autour
des arbres
Nous présentons dans cet exposé un algorithme
général pour la résolution de contraintes du
premier ordre dans des théories dites "décomposables".
Tout d'abord, en utilisant des quantificateurs spéciaux, nous
donnons une caractérisation formelle des théories
décomposables et montrons quelques unes de leurs
propriétés. Nous présentons ensuite un algorithme
général pour la résolution de contraintes du
premier ordre dans une théorie décomposable "T"
quelconque. L'algorithme est donné sous forme d'un ensemble de
cinq règles de réécriture. Il transforme une
formule "a", qui bien entendu peut contenir des variables libres, en
une conjonction "b" de formules résolues, équivalente
dans T et ne faisant pas intervenir d'autre variables libres que celle
de "a". Cette conjonction de formules résolues est soit la
formule "vrai", soit la formule "faux", soit contient au moins une
variable libre et n'est équivalente ni à "vrai" ni
à "faux". En particulier, si "a" n'a pas de variables libres
alors "b" est soit la formule "vrai" soit la formule "faux". La
correction de notre algorithme démontre la complétude des
théories décomposables.
Nous donnons ensuite une manière automatique pour mélanger une théorie T quelconque avec la théorie des arbres et montrons que sous certaines conditions très simples sur T et uniquement sur T le mélange T+arbre donne une théorie décomposable et donc complète. Nous terminons alors notre exposé par une série de benchmarks réalisées par une implantation de notre algorithme résolvant des formules sur des jeux à deux partenaires qui font intervenir des imbrications de plus de 160 quantificateurs alternés dans une théorie combinant les arbres aux rationnels additifs ordonnées (Q,+,-,<).
Jeudi 17 novembre 2005:
10h30 Jacques Cohen,
Brandeis University, Waltham, MA, USA
Towards a comprehensive view of
computational approaches in systems biology.
In the past few years the number of available papers describing
computational approaches in systems biology has increased
significantly. These approaches vary considerably from one another. In
this talk we aim to provide a birds eye view of the various methods
that have been proposed to analyze and infer gene regulatory networks.
In so doing we are bound to find novel combined approaches that are
worth pursuing.
A rough initial classification of the current methods distinguishes
between discrete and continuous, stochastic (probabilistic) and
non-stochastic, analysis (forward) and inference (reverse engineering).
Starting from discrete methods of analysis (e.g., Thomas, Thieffry, de
Jong) we proceed to cover existing probabilistic (e.g., Shmulevich) and
reverse engineering approaches (e.g., Akutsu, Somogyi) including those
based on perturbation (e.g., Karp, Collins).
One of the findings based on this comprehensive view is that it is
worth considering model-checking as a filter for networks being tested
as possible candidate in the reverse engineering process. Another
finding suggests a perturbation method for translating continuous
models into discrete ones. We conclude by raising a few relevant
questions about research directions in systems biology that are worth
exploring.
(Work done jointly with Sam Blasiak; the talk is directed to computer scientists with no advanced knowledge in biology)
Vendredi 14 octobre 2005:
10h30 Carolyn Talcott
(Stanford Research Institute, USA)
Pathway Logic: Application of Formal
Modeling Techniques to Understanding Biological Signaling Processes.
Pathway Logic is an application of techniques from formal
methods to
the modeling and analysis of signal transduction networks in mammalian
cells.
These signaling network models are developed using Maude, a formal
language and
execution environment founded on rewriting logic. Network elements
(reactions)
are represented as rewrite rules. Models can be queried (analyzed)
using the
execution, search and model-checking tools of the Maude system.
Alternatively,
models can be exported as Petri Nets for analysis using tools
specialized for
Petri Nets. The Pathway Logic Assistant (PLA) is a tool for browsing and
querying Pathway Logic models via an interactive graphical
representation. A
model can be queried to find relevant subnetworks and pathways leading
to
situations of interest. Situations to be avoided can be specified
allowing the
user to explore knockouts and alternative pathways.
<>
In the talk we will give a brief introduction to Rewriting Logic,
Maude, and
the associated analysis techniques. We will then explain how biological
signaling networks are represented, both textually and the interactive
graphical representation of the PLA. The ideas will be illustrated
using a
curated model of signaling in human mammary epithelial cell. A link to
downloads of the Pathway Logic Assistant (Linux and Mac OS X), a sample
model, and some tutorial materials can be found on the Pathway Logic
website
[http://www.csl.sri.com/~clt/PLweb/].
Lundi 13 juin 2005:
10h30 Albert Goldbeter
(Université libre de Bruxelles)
Modélisation des rythmes
circadiens: Du mécanisme moléculaire aux troubles du
sommeil
Les rythmes circadiens proviennent de boucles de rétroaction entremêlées au sein de réseaux de régulation génétique. Des modèles de complexité croissante ont été proposés pour le mécanisme moléculaire de ces rythmes qui se produisent spontanément, avec une période proche de 24 heures. Des modèles déterministes pour les rythmes circadiens chez la drosophile rendent compte de propriétés dynamiques telles que le déphasage ou la suppression des rythmes par une impulsion lumineuse, et l’entraînement par des cycles lumière-obscurité. Une version stochastique de ces modèles permet de tester la robustesse des oscillations circadiennes par rapport au bruit moléculaire. L’extension de la modélisation à l’horloge circadienne des mammifères contribue à clarifier les bases dynamiques de certains troubles du cycle veille-sommeil chez l’homme.
Vendredi 27 mai 2005:
10h30 Richard Lassaigne
(Université Denis Diderot Paris 7)
Vérification probabiliste et approximations
Model checking is an algorithmic method allowing to automatically
verify if a system which is represented as a Kripke model satisfies a
given specification. Specifications are usually expressed by formulas
of temporal logic. The first objective of this talk is to give an
overview of methods able to verify probabilistic systems. Models of
such systems are labelled discrete time Markov chains and
specifications are expressed in extensions of temporal logic by
probabilistic operators. The second objective is to focus on the
complexity of these methods and to answer the question: can
probabilistic verification be efficiently approximated? In general, the
answer is negative. However, in many applications, the specification
formulas can be expressed in some positive fragment of linear time
temporal logic. In this paper, we show how some simple randomized
approximation algorithms can improve the efficiency of the verification
of such probabilistic specifications.
Mardi 3 mai 2005:
14h00 Vladislav Vyshemirsky (University of Glasgow, Scotland)
Analysis of signalling pathways using the PRISM model checker
We describe a new modelling and analysis approach for signal transduction networks in the presence of incomplete data. We illustrate the approach with an example, the RKIP inhibited ERK pathway.
Our models are based on high level descriptions of continuous time Markov chains: reactions are modelled as synchronous processes and concentrations are modelled by discrete, abstract quantities. The main advantage of our approach is that using a (continuous time) stochastic logic and the PRISM model checker, we can perform quantitative analysis of queries such as if a concentration reaches a certain level, will it remain at that level thereafter? We also perform standard simulations and compare our results with a traditional ordinary differential equation model. An interesting result is that for the example pathway, only a small number of discrete data values is required to render the simulations practically indistinguishable.
Mercredi 13 avril 2005:
11h00 Erik Sandewall
(Linköping University, Suède)
Renaissance
et Reforme dans le Domaine du Logiciel
The work reported here is performed in a broader context where
we propose to change the overall software architecture (operating
systems, programming languages, etc etc) in order to eliminate the
considerable redundancy of concepts and constructs that contemporary
software technology exhibits. This requires, among other things, a
realignment so that some constructs that used to be placed on higher
levels of software now become incorporated in a kernel on a much lower
level.
In this framework, we propose in particular to use the construct of an *action* already in the kernel, whereby it
becomes available for many applications as a conceptual and
computational resource and in a uniform fashion. The article describes
and discusses the ramifications of this approach, including how it
relates to the current state of the art in logics of actions and
change, as well as the nonmonotonic character of one of its
computational constructs.
Vendredi 25 février 2005:
10h30 Kazunori Ueda
(Waseda University, Tokyo)
LMNtal: a Language Model with Logical
Links and Membranes
LMNtal (pronouned "elemental") is a
simple language model based on graph rewriting that uses logical
variables to represent links and
membranes to represent hierarchies. The
two major goals of LMNtal are
(i) to unify various computational models based on multiset rewriting
and (ii) to serve as the basis of a truly general-purpose language
covering various platforms ranging from wide-area to embedded
computation. Another contribution of the model is it greatly
facilitates programming with dynamic data structures.
LMNtal is an outcome of the attempt to unify two extensions of
concurrent logic programming, namely concurrent constraint programming
and Constraint Handling Rules, where our focus has been multiset
rewriting rather than constraint handling. At the same time, LMNtal can
be regarded as a hierarchical multiset rewriting language augmented
with logical links, and many computational models including Petri Nets,
Gamma, the pi-calculus, etc., can be encoded into LMNtal.
Yet another view of LMNtal is a constructor-free linear concurrent
logic language in which data structures are encoded as process
structures. Constructor-freeness means that LMNtal links are
zero-assignment variables, where the purpose of a variable is to
connect two points using a private identity. Multisets are supported by
the membrane construct that allows both nesting and mobility. Logical
links can represent (among other things) communication channels, but
the key differences from pi-calculus channels are that
(i) a message sent through a link changes the identity of the link and
(ii) links are always private.
The LMNtal system, running on a Java platform, has been released and
the talk will include animating demonstrations of the system in
addition to language issues.
Mercredi 5 janvier 2005:
10h30 Benno Schwikowski
(Institut Pasteur)
Computational Systems Biology at
Institut Pasteur: Enabling high-throughput mass spectrometry, and
integrating heterogeneous data in large-scale interaction networks
This talk will highlight the two major areas of interest of our new
research Unite at Institut Pasteur. The first part of the talk will
focus on the dev
elopment of new measurement approaches, in particular a
novel way to interpret data acquired from mass spectrometry (MS)
analysis of very complex samples. Typically, multidimensional liquid
chromatography (LC) is used to separate such samples into fractions of
lower complexity. Until now, the multidimensional structure among
samples has not been used, but we will demonstrate how dimensionality
can be exploited to improve many aspects of the
experimental-computational protocol for identifying and quantifying
proteins on a large scale.
Our second interest lies in the integration of heterogeneous data types
in molecular interaction networks. We will present a novel approach to
find sequence motifs relevant for protein interactions. In addition to
sequence information, an experimentally determined large-scale
interaction network is used. The introduction of this new type of data
allows the efficient usage of a more complex and realistic model for
biologically and medically important families of proteins, and leads to
improved predictions of protein interactions.
Jeudi 25 novembre 2004:
14h00-17h00 André Gagalowicz (projet MIRAGES)
Modélisation texturelle.
Vendredi 19 novembre 2004:
14h00 Luc de Raedt (University of Freiburg, Allemagne)
An overview of some traditional ILP
systems that might be of interest to Biocham
Mardi 5 octobre 2004:
10h30 Yann Georget (Koalog)
Présentation et architecture de
Koalog Constraint Solver
Dans cet exposé,
je présenterai Koalog Constraint Solver, une bibiothèque
Java pour la programmation par contraintes. Après avoir
justifié le choix du langage (Java) et la forme
(bibiothèque), je passerai en revue plusieurs choix
d'architecture pour la réalisation de Koalog Constraint Solver :
couches logicielles, généricité du noyau de base,
ordonnancement des contraintes, références
backtrackables,
. . . Koalog Constraint Solver étant optimisé pour les
contraintes globales, je détaillerai l'une d'elles, la
contrainte
Disjunctive (pour l'ordonnancement disjonctif). Enfin, je donnerai
quelques résultats concernant les performances de Koalog
Constraint Solver et présenterai quelques axes de R&D.
Vendredi 1er octobre 2004 (salle de conférence du
bâtiment *11*):
10h30 Jean Clairambault (INRIA-INSERM Villejuif))
Modéliser l’apoptose : buts,
questions, outils
Vendredi 17 septembre 2004:
10h30 Laurence Calzone (INRIA, Post-doc ARC CPBIO)
How could learning methods for
parameter estimation assist biologists/modelers?
We propose to present an example of a generic kinetic model of the
mammalian cell cycle. We will expose the different problems
raised
by fitting the experimental data and the techniques used in
developing such numerical models. General ideas on how automated
ways in parameter search could assist the biologist will be developed.
Mardi 20 juillet 2004:
10h30 Laurence Calzone (Budapest, Hungary & Virginia State
University)
Modélisation mathématique du cycle cellulaire chez la
levure et la drosophile.
Des modèles
mathématiques ont été réalisés dans
le but de décrire les mécanismes de régulation du
cycle cellulaire chez les levures (Saccharomyces cerevisiae et Schizosaccharomyces
pombe) et les mammifères. Ces modèles
représentent essentiellement des interactions entre
protéines menant à la division cellulaire. Beaucoup de
ces
réseaux de protéines se retrouvent dans les cellules
somatiques et embryonnaires de plusieurs eucaryotes. Cependant, la
régulation de ces deux types de cellules présente des
aspects différents et inattendus selon l'organisme. Ainsi, nous
proposons d'étudier en détails les cycles cellulaires
embryonnaires de la drosophile (Drosophila melanogaster). Juste
après la fécondation, une série de treize cycles
est observée suivie d'un arrêt en phase G2. Durant ces cycles rapides et synchronisés, les noyaux
se divisent mais continuent de partager le même cytoplasme. Le
fait le plus singulier est que, durant ces divisions, la
quantité totale du complexe Cdk1/CycB (aussi appelé MPF)
n'oscille que dans les derniers cycles, ce qui est contraire aux
observations et au rôle associés à ce complexe. En
effet, les cycles de divisions nucléaires sont
généralement régulés
par l’activité des complexes Cdk1/CycB.
Après une courte
présentation d'un modèle du cycle cellulaire chez la
levure, je proposerai un modèle décrivant les treize
cycles cellulaires chez la drosophile. Quelques modifications d'un
modèle déjà existant de Xenopus (telles
que compartimentation et dégradation locale de certaines
composantes du système) permettent de simuler des
phénomènes observés expérimentalement.
Vendredi 14 mai 2004, Bâtiment 1, amphithéatre
Turing:
9h30-16h30 Revue finale du projet RNTL OADymPPaC
Outils pour l'Analyse Dynamique et la mise au Point de Programmes
avec
Contraintes
9.30 Café d'accueil
10.00 Introduction
10.15 Présentations techniques et
démos
11.30 Pause
11.45 Présentations techniques et
démos 13.00 Déjeuner sur place
(sur invitation)
14.30
Présentations techniques et/ou Discussion avec
les experts
15.30 Pause et clôture des exposés
16.00
Discussion ouverte (travaux futurs)
16.30
Clôture
Programme détaillé sur
http://contraintes.inria.fr/OADymPPaC/Public/Revue/progr.html
Lundi 8 mars 2004:
10h30 Alexandre Frey (Trusted Logic)
Problèmes de contraintes pour le sous-typage en monde
ouvert.
L'exposé portera sur une partie de mon travail de thèse.
J'ai étudié le typage à la ML d'un langage d'ordre
de supérieur avec objets, multi-méthodes, et sous-typage.
Une approche algébrique m'a permis de réduire de
façon générique le typage à un
problème de contraintes. La correction du typage est
montrée moyennant quelques axiomes minimaux sur l'algèbre
domaine d'interprétation de ces contraintes.
Cette réduction est indépendante du modèle
effectivement utilisé pour interpréter les contraintes.
J'ai utilisé cette propriété pour décrire
finement le typage de l'aspect "monde ouvert" des langages à
objets. Cette caractérique essentielle permet d'utiliser un
module dans un "monde" qui n'est pas connu au moment de son
écriture.
Je discuterai de la description de cet aspect en terme de
quantification sur le modèle utilisé pour
interpréter les contraintes (quantification sur toutes les
extensions possibles). Je tenterai une classification des
problèmes obtenus. Nous pourrons ensuite discuter de leur
originalité et des connections avec d'autres domaines, en
particulier la programmation logique par contraintes.
Lundi 5 janvier 2004:
14h00 François Fages (INRIA Rocquencourt)
La machine abstraite biochimique BIOCHAM: un pas vers une
biologie formelle.
La biologie est clairement engagée dans un
travail d'élucidation des processus biologiques de haut niveau
en
termes de leurs bases biochimiques à l'échelle
moléculaire. La production en masse de données
post-génomiques (expression génique, synthèse de
protéines, intéractions
protéines-protéines,
etc.) soulève le besoin d'un effort parallèle important
sur la représentation formelle des processus biochimiques et de
leur dynamique globale.
Dans cet exposé nous proposons un langage simple de
modélisation de processus biochimiques et l'utilisation de la
logique temporelle CTL comme langage d'expression des
propriétés biologiques d'un système. Nous montrons
que les techniques de vérification symbolique de modèles
(issues de la preuve de circuits et de programmes concurrents)
s'appliquent aux réseaux biochimiques, et qu'elles
présentent certains avantages sur la simulation pour interroger
et valider des modèles formels de processus biologiques. Nous
dresserons un bilan de nos expériences sur la conception du
langage BIOCHAM à travers la modélisation et
l'interrogation de plusieurs exemples de processus biochimiques, dont
un
modèle qualitatif du contrôle du cycle cellulaire chez les
mammifères.
(Travail joint avec Nathalie Chabrier-Rivier et Sylvain Soliman en
collaboration avec l'ARC CPBIO)
Lundi 18 août 2003:
11h00 Stephen Muggleton (Imperial College, Londres)
Inductive logic programming in bioinformatics.
We present the inductive logic programming system
Progol and relate our experience of using Progol in two applications in
bionformatics: one in the functional genomics of the yeast, and one for
predicting the toxicity of proteins.
Vendredi 6 décembre 2002, lieu: Paris, Université
Paris 6,
Salle C769, 8 rue du Capitaine Scott, 75015 Paris (Metro
Dupleix)
15h00 Vincent Devloo (SCMBB, Faculté des Sciences de
Bruxelles)
Vers la modélisation du réseau des processus
cellulaires
L'Analyse Logique Généralisée
(René Thomas et collaborateurs) est
une théorie permettant de mettre en évidence des
comportements
multistationnaires et périodiques dans le cadre de la
modélisation de
réseaux génétiques. Elle permet ainsi de
caractériser la différentiation
et l'homéostasie. Dans le cadre de mon travail de thèse,
une
reformalisation de la théorie ainsi que l'utilisation de la
programmation
par contraintes ont permis de rendre la théorie accessible
à des systèmes
beaucoup plus grands que précédemment. Je présente
aussi un logiciel de
modélisation permettant le "reverse engeenering" et
l'expérimentation virtuelle. Enfin, deux applications
tirées de la
littérature sont examinées à l'aide des outils
théoriques et logiciels
développés, dont l'une concerne un réseau non
génétique afin de mettre en
évidence la pertinence de la théorie dans un cadre plus
général.
Jeudi 8 août 2002:
11h00 Rafaël Ramirez-Melendez (INRIA Rocquencourt)
A constraint-based methodology for concurrent programming
The task of programming concurrent systems is
substantially more
difficult than the task of programming sequential systems
with respect
to both correctness and efficiency. In this talk we
describe a
constraint-based methodology for writing concurrent
applications.
A system is modeled as: (a) a set of processes containing
a sequence
of markers, denoting the processes points of interest; and
(b) a
constraint store. Process synchronization is specified
declaratively
by incrementally adding constraints on the markers'
execution order
into the constraint store. The store, thus, acts as a
coordination
entity which on the one hand encapsulates the system
synchronization
requirements, and on the other hand, provides a
declarative
specification of the system concurrency issues. This
provide great
advantages in writing concurrent programs and manipulating
them
while preserving correctness.
Lundi 10 décembre 2001:
11h00 Arnaud Courtois (LORIA, Nancy)
Modélisation de systèmes biologiques en
programmation par contraintes
L'exposé essaiera de montrer que l'utilisation de la
programmation
concurrente par contraintes hybrides est à même de
reproduire
différentes techniques de modélisations usuelles en
biologie.
Après un bref résumé du contexte qui nous
intéresse, seront
présentés le langage de programmation utilisé,
différents modèles
dynamiques, ainsi que des exemples de modélisations.
La conclusion portera sur les limites de la modélisation, en
particulier
les possibilités de raffinement ou les obligations de
simplification.
13h30 Vincent Danos (CNRS, PPS Paris)
Communication et Controle: le EEP-calculus
On construit un modèle de communication, le EEP-calcul,
du type PI-calcul ou JOIN-calcul appliqué (c'est-à-dire
avec "locations").
A la différence des modèles usuels, les processus
résidents
exercent un contrôle sur les processus mobiles, avec notamment la
possiblité de transformer dynamiquement les noms d'un agent
(masquerading).
Environnements agressifs, rapiéçage (patch) dynamique,
séquestration de
processus mobiles ont une représentation simple dans le calcul.
Jeudi 8 novembre 2001:
11h00 Pierre Boullier (INRIA Rocquencourt)
Les grammaires à concaténation d'intervalles
Ce séminaire va être consacré à la
présentation des grammaires à concaténation
d'intervalles (range concatenation grammars -- RCG). C'est un
formalisme
syntaxique qui est à la fois simple, puissant et efficace.
En fait, les RCG
définissent exactement la sous-classe des langages
dépendant du contexte qui
peut s'analyser en temps polynomial. Bien sûr, cette
sous-classe contient les
langages non-contextuels, mais aussi, par exemple, les langages «
mildly
context-sensitive », célèbres en traitement de la
langue naturelle. D'autre
part, les RCG ont des propriétés de fermeture
(clôture par intersection et
complémentation) qui les rendent modulaires.
Les applications déjà réalisées montrent
que les temps d'exécution des
analyseurs produits, fonction polynomiale de la longueur du source,
sont
particulièrement compétitifs. Outre les langues
naturelles, Les RCG pourraient
trouver des applications en biologie (prédiction des structures
secondaires de
l'ARN ou de protéines), ou même servir de base
à une "extension" des DCG.
Mardi 12 juin 2001:
14h00 Hubert Dubois (LORIA Nancy)
Programmer avec des objets et des contraintes en ELAN
Partant d'une volonté de développer des
systèmes de règles de
production en calcul de réécriture, nous avons
dégagé un
formalisme de règles travaillant sur une mémoire de
travail composée
d'objets et coopérant avec une base de contraintes.
L'application de cet ensemble de règles est
contrôlé par
des stratégies.
Le système ELAN est un environnement reposant sur le
paradigme de
règles et stratégies. Le calcul de
réécriture est un nouveau calcul
permettant de définir une sémantique uniforme dans
laquelle on peut
exprimer à la fois les termes et le concept d'application de
règles
sur ces termes. Le calcul de réécriture fournit une
sémantique
opérationnelle au système ELAN.
On a donc développé une extension objet pour le
langage ELAN
respectant la sémantique du calcul de réécriture,
ainsi qu'un
formalisme de règles permettant de manipuler à la fois
objets et
contraintes associées. L'ensemble forme un nouveau
paradigme de
programmation permettant de modéliser des problèmes de
planification
ou d'ordonnancement par exemple.
11h00-12h00 Dale Miller, CSE, Penn State
Encoding Generic Judgments
14h00-14h45 Jeremie Wajs, CSE Penn State
Reasoning about logic programs
14h45-15h30 Sorin Craciunescu, INRIA Rocquencourt
A Soundness Proof of a Formal System for Equivalence of Logic
Programs
11h00-12h00 Catuscia Palamidessi, CSE, Penn State
(joint work with Oltea Mihaela)
Challenges and Promising Directions in the Distributed
Implementation of Choice
14h00-14h45 Frank Valencia, BRICS, Aarhus, Danemark
(joint work with Catuscia Palamidessi , CSE, Penn State)
A Calculus for Temporal Constraint Programming
14h45-15h30 Lionel Kalill, ENS Paris
(joint work with Maribel Fernandez)
Reseaux d'interaction avec ambiguite
Vendredi 20 avril 2001 (Université Paris 7 Chevaleret
salle 1C6):
10h30 Soutenance de thèse de Sylvain Soliman (INRIA
Rocquencourt, Univ. Paris 7)
Programmation concurrente avec contraintes et logique
linéaire
Dans cette thèse, nous étudions les liens
étroits entre la logique
linéaire et la programmation concurrente par contraintes, sous
l'angle de la
sémantique, et plus précisément de la
vérification de programmes.
Nous raffinons les observables caractérisables grâce a
la logique linéaire et
étendons des résultats antérieurs, afin d'obtenir
une sémantique plus précise
et plus générale. Ces résultats sont obtenus par
une traduction plus fidèle des
agents en formules logiques et un enrichissement de la théorie.
Nous présentons aussi une méthode originale de preuves
de programmes, basée sur
la sémantique de la prouvabilité de la logique
linéaire: la sémantique des
phases. Celle-ci nous donne un outil de vérification avec de
nombreuses bonnes
propriétés: la possibilité de montrer une
propriété universelle du programme
simplement par un contre-exemple; une facilite d'abstraction; enfin la
simplicité des preuves obtenues.
Nous construisons donc une méthode systématique de
preuve et, après l'avoir
testée avec succès sur des exemples classiques, nous
étudions son
automatisation. Cette étude aboutit a l'implémentation
d'un prototype de
prouveur qui accompagne un interpréteur pour les langages
linéaires concurrents
avec contraintes.
14h00 Catuscia Palamidessi (CSE, Penn State, USA)
(Joint work with Mihaela Herescu)
On the generalized dining philosophers problem.
The problem of the dining philosophers, proposed by Dijkstra, is a
very popular example of control problem in distributed systems. In the
classic
formulation the philosophers sit at a round table and there is a fork
between
any two philophers. In order to eat, each philosopher needs both his
adjacent
forks. The aim is to make sure that if there are hungry philosophers
then some
of them will eventually eat (deadlock freedom), or, more ambitiously,
that
every hungry philosopher will eventually eat (lockout freedom).
In the early 80's, Lehman and Rabin showed that there exist no
deterministic,
fully distributed and symmetric solution to the problem of the dining
philosophers, and they proposed two randomized solutions: one which
guarrantees
deadlock freedom with probability 1 and another one which guarrantees
lockout
freedom with probability 1.
In this talk, we consider a generalization of the dining
philosophers problem
where the number of philosophers can exceed the number of forks
(although each
philosopher can still only access two forks), and we study whether the
randomized algorithms of Lehman and Rabin still work in this situation.
We show
that the answer is "No": in most cases, a malicious scheduler can
induce a
deadlock. We then show a randomized solution, still fully distributed
and
symmetric, which works for any number of philosophers and any kind of
connection graph, and guarrantees lockout freedom with probability 1.
Jeudi 8 mars 2001:
10h30 Dao Thi Bich Hanh (LIM, Marseille)
Résolution de contraintes du premier ordre dans la
théorie des arbres finis ou
infinis
Le sujet de cet exposé est la résolution de
contraintes dans la théorie complète
T des arbres éventuellement infinis. Ces contraintes se
présentent sous forme de
formules générales du premier ordre construites à
partir d'un ensemble infini de
symboles d'opérations et de l'égalité. Par,
résoudre une contrainte p dans T,
nous entendons : transformer p en une contrainte q équivalente
dans T, qui est la
constante logique Vrai si p est toujours vraie dans T, est la constante
Faux si p
est toujours fausse dans T. De plus, si p ou sa négation a une
base fini de
solutions dans un modèle de T, alors ces solutions ou
non-solutions doivent être
explicites dans q.
Après avoir introduit l'algèbre des arbres et
montré qu'elle constitue bien un
modèle de la théorie des arbres, nous montrons que nos
contraintes ont un pouvoir
d'expression << quasi-universel >> et proposons un
algorithme en 11 règles de
réécriture de sous-formules pour les résoudre.
Nous considérons ensuite la
structure obtenue en introduisant dans cette algèbre un
prédicat unaire fini(x),
exprimant que x est un arbre fini. Nous proposons une extension TuFINI
de la
théorie T admettant cette structure comme modèle. Nous
donnons un algorithme pour
résoudre les contraintes dans TuFINI en 16 règles de
réécriture et concluons
ainsi que TuFINI est une théorie complète. Nous donnons
également un système de
12 règles de réécriture qui effectue le même
type de résolution de contraintes
dans la théorie des arbres finis. Nous terminons par des
détails sur
l'implantation d'algorithmes de résolution de contraintes, dans
la théorie T des
arbres éventuellement infinis et dans la théorie des
arbres finis. Les exemples
qui nous ont servi à montrer le pouvoir d'expression de nos
contraintes nous
permettent de produire des benchmarks intéressants.
Mardi 27 février 2001:
14h00 Slim Abdennadher (Univ. Ludwig Maximilian de Munich)
Automatic Generation of Rule-based Constraint Solvers
A general approach to implement propagation and simplification of
constraints consists of applying rules over these constraints.
However, a difficulty that arises frequently when writing a
constraint solver is to determine the constraint propagation
algorithm. In this talk, we present a method for generating
propagation and simplification rules for constraints over finite
domains defined extensionally by e.g. a truth table or their
tuples. The generation of rules is performed in two steps.
In a
first step, only propagation rules are generated. This method is
inspired by techniques used in the field of knowledge
discovery. In a second step, some propagation rules are
transformed
into simplification rules. The method is based on a confluence
notion, i.e. a technique adapted from rewriting systems.
Using our
algorithm, the user has the possibility to specify the
admissible
syntactic forms of the rules. The generated rules will be
implemented as rules of the language Constraint Handling Rules.
Jeudi 23 novembre 2000:
10h30 Tomasz Truderung (University of Wroclaw, Pologne)
Polymorphic Directional Types.
We present a directional, polymorphic, rule based type system for
logic programming languages. We discuss the notion of main type and
present the main type reconstruction algorithm. We describe the current
state of implementation, and show some sample runs of our algorithms.
We
analyse their practical time complexity. We also discuss the
possibility
of embedding our system in real life languages such as Prolog.
13h30 Emmanuel Coquery (INRIA)
Typed Constraint Logic Programs:
checking domain coercions and metaprograms through subtyping.
We propose a general prescriptive type system with parametric
polymorphism and subtyping for constraint logic programs. The aim
of this type system is to detect programming errors statically. It
introduces a type discipline for constraint logic programs and modules,
while maintaining the capabilities of performing the usual coercions
between constraint domains and of typing meta-programming predicates,
thanks to the flexibility of subtyping. The property of subject
reduction expresses the consistency of the type system w.r.t. the
execution model: if a program is ``well-typed'', then all derivations
starting in a ``well-typed'' goal are again ``well-typed''. That
property is proved w.r.t. the abstract execution model of constraint
programming which proceeds by accumulation of constraints. We
describe our implementation of the system for type checking and type
inference. We report our experimental results on type checking
the
libraries of Sicstus Prolog and other Prolog programs.
Mercredi 13 septembre 2000, bâtiment 16:
10h30 Rajeev Goré, Australian National University.
CardKt: Automated Multi-modal Deduction on Java Cards for
Multi-application Security.
We describe an implementation of a Java program to perform automated
deduction in propositional multi-modal logics on a Java smart
card. The tight space limits of Java smart cards make the
implementation non-trivial. A potential application is to ensure that
applets down-loaded off the internet conform to personalised
security permissions stored on the Java card using a security
policy encoded in multi-modal logic. In particular, modal logic
may be useful to ensure that previously checked ``trust''
relationships between addition of a new applet. That is, by using
multi-modal logic to express notions of permissions and obligations, we
can turn the security check into an on-board theorem proving task. Our
theorem prover itself could be down-loaded ``just in time'' to perform
the check, and then deleted to free up space on the card once the
check has been completed. Our work is thus a ``proof of
principle'' for the application of formal logic to the security of
multi-application Java cards.
11h00-12h00 Dale Miller, CSE, Penn State
Encoding Transition Systems in Sequent Calculus
14h00-14h45 Jeremie Wajs, CSE Penn State
A theorem prover for operational semantics
14h45-15h20 Sorin Craciunescu, INRIA Rocquencourt
Proofs by Coinduction for Logic Programs
15h40-16h20 Sylvain Soliman, INRIA Rocquencourt
Semantics and Precision
11h00-12h00 Catuscia Palamidessi , CSE, Penn State
Concurrent Constraint Programming with Process Mobility
14h00-14h45 Oltea Mihaela Herescu, CSE, Penn State.
Probabilistic Asynchronous Pi-Calculus
14h45-15h30 Lionel Khalil, ENS Paris
Generalization of Interaction Nets with a Unique Parallel Agent
Mardi 23 mai 2000
10h30 Daniel Diaz, INRIA, Univ. Paris 1.
GNU-Prolog: un compilateur natif pour Prolog intégrant un
résolveur decontraintes sur les domaines finis.
Nous présenterons le système GNU-Prolog, un
compilateur natif pour le langage Prolog incluant un puissant
résolveur de contraintes sur les domaines finis. Le
système GNU-Prolog a été retenu par GNU pour etre
le Prolog officiel de cette organisation. Après un aperçu
général de GNU-Prolog, nous détaillerons le
schéma de compilation de GNU-Prolog. Celui-ci est basé
sur
un langage intermédiaire de bas niveau qui reste toutefois
indépendant de la machine. Un programme Prolog+contraintes est
donc compilé vers ce langage qui est ensuite traduit vers
l'assembleur de la machine cible. Cette dernière étape
est
simplifiée du fait que ce langage intermédiaire est
basé sur un jeu d'instructions réduit. Enfin, nous
montrerons quelques aspects du résolveur de contraintes sur les
domaines finis de GNU-Prolog et, en particulier, le langage de
description de contraintes permettant à l'utilisateur de
définir de nouvelles contraintes si nécessaire.
Jeudi 13 avril 2000
14h Jean-Pierre Banâtre, INRIA Dir. UR Rocquencourt.
Gamma et la programmation par transformation de multi-ensembles.
Gamma fut propose a l'origine en 1986 comme
un formalisme pour la definition de programmes non
sequentiels. L'idee de base sous-jacente au formalisme consiste a
decrire le calcul comme une forme de reaction chimique dans une
solution
de donnees individuelles. De par la nature tres minimale du
langage, et l'absence de biais sequentiel, il a ete
possible
d'exploiter le paradigme initial dans diverses
directions. Dans cet expose nous ferons un survol des
travaux effectues dans ce domaine, en insistant sur
1) la programmation parallele par transformation de multi ensembles,
2) l'interet du modele de reaction chimique,
3) les extensions du modele d'origine et
4) les questions d'implementation. multi-ensembles.
Jeudi 2 mars 2000
14h00 Aviv Regev, Udi Shapiro, Weizmann Institute.
Representing Biomolecular Processes with Process
Algebra:pi-Calculus as a Formalism for Signal Transduction Networks
Molecular processes, such as gene expression, metabolism and signal
transduction (ST) networks play a key role in the normal and
pathological function of cells, tissues and organisms. However,
while biomolecular sequence and structure information has an objective
representation that is amenable to critical evaluation and computer
manipulation, knowledge of biomolecular processes has so far eluded
such
representation and study. We propose to treat these molecular
systems as concurrent computational processes using process algebras.
In
particular, we show that complex ST pathways can be represented
formally
in the pi-calculus. pi-calculus representations of ST unify
dynamic behavior and function of pathways with the molecular details
that underly this behavior. They provide a comprehensive model of ST,
which is both mathematically well-defined and biologically visible.
This
model is amenable to simulation studies, analogous to mutational
manipulation and experimentation, as well as to formal verification and
analysis. Furthermore, based on notions of behavioral equivalence,
pathways may be compared to each other, and a novel measure of
homology,
the "homolgy of process" can be established. Thus, adopting such a
common formalism may facilitate our understanding of the function and
evolution of biomolecular processes.
Mercredi 23 février 2000: Journée
"Contraintes et Chaos", Bâtiment 16
9h30 Arnaud Lallouet, LIFO Orléans
Une sémantique co-inductive pour la propagation de
contraintes et le labeling.
10h30 Gérard Ferrand, LIFO Orléans
Relaxation parfaite de contraintes.
11h30 François Fages, INRIA
Propagation de contraintes et itération chaotique.
Mardi 8 février 2000
14h-15h Pierre-Etienne Moreau, Bouygues DTN.
Compilation de regles de reecriture et de strategies
non-deterministes'
Les techniques de réécriture ont été
développées depuis les années 1970 et
appliquées en particulier au prototypage des
spécifications formelles algébriques et à la
démonstration de propriétés liées à
la vérification de programmes.
ELAN est un système qui permet de spécifier et
d'exécuter des démonstrateurs, des résolveurs de
contraintes et plus généralement tout processus
décrit par des règles de transformation. Il
possède
des opérateurs associatifs-commutatifs (AC) et un langage de
stratégies qui permettent une gestion fine de l'exploration d'un
arbre de recherche et une manipulation aisée d'opérateurs
mathématiques tels que les connecteurs booléens, les
opérateurs arithmétiques ou les opérateurs de
composition parallèle par exemple.
Ces deux notions améliorent grandement l'expressivité
du langage mais introduisent un double non-déterminisme
lié à la possibilité d'appliquer plusieurs
règles, de différentes façons, sur un terme
donné. Cela rend difficile et généralement peu
efficace leur implantation.
L'objectif principal de ce travail est d'étudier des
techniques de compilation qui améliorent l'efficacité de
ce type de langages. Nous proposons un nouvel algorithme, à base
d'automates déterministes, pour compiler efficacement le
filtrage
syntaxique. Nous définissons ensuite différentes classes
de règles pour lesquelles nous proposons un algorithme efficace
de filtrage AC. Cet algorithme utilise une structure de donnée
compacte et les automates définis précédemment, ce
qui améliore considérablement les performances du
processus de normalisation dans son ensemble.
L'étude du langage de stratégies conduit à
implanter des primitives originales de gestion du backtracking et
à définir un algorithme d'analyse du déterminisme
permettant de réduire leur usage et d'améliorer encore
les
performances, tout en réduisant l'espace mémoire
nécessaire. Enfin, l'implantation des méthodes
proposées a donné lieu à l'élaboration de
nombreuses optimisations théoriques et techniques qui peuvent
être largement réutilisées pour implanter d'autres
langages de programmation par réécriture.
.