*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h30                     *
*                           Salle S16, etage -1                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

***  Vendredi 23 mars 2007, 14h00-15h00 *****************************

Je'ro^me Feret (ENS-DI)
Accessibilit'e et simplification automatique de mod`eles kappa - BNG

Re'sume' :

Le calcul kappa - BNG est un syst`eme de r'e'ecriture de graphes, qui
permet de d'{'e}crire des cascades de transmissions de messages entre
cellules. Dans ces graphes, les noeuds repr'esentent des prot'eines.
Ces prot'eines ont un 'etat interne (des bool'eens) et peuvent se lier
deux `a deux via des sites de liaisons.

Nous utilisons l'interpr'etation abstraite pour surapproximer les
complexes prot'eiques qui peuvent se former. Le r'esultat de cette
analyse nous permet de simplifier les syst`emes de r`egles tout en
pr'eservant leur syst`eme de transitions.

Notre analyse d'accessiblit'e est tr`es pr'ecise. Nous donnons des
conditions suffisantes sur les syst`emes de r`egles pour que l'analyse
calcule exactement l'ensemble des complexes accessibles. Les syst`emes
de r`egles simplifi'es v'erifient ces conditions plus souvent.

Toutes ces analyses sont implant'ees dans l'outil Complx que nous
utiliserons sur deux exemples: EGF(facteur de croissance 'epidermique)
et FGF (facteur de croissance du Fibroblaste).

Travail commun (par ordre alphab'etique): Vincent Danos, J'er^ome
Feret, Walter Fontana, Jean Krivine.
Harvard Medical School
Plectix Biosystems
'Ecole Normale Sup'erieure

***

Je'ro^me Feret (ENS-DI)

Reachability analysis and automatic simplification of kappa - BNG models.

Abstract:

The  kappa - BNG calculus is a graph rewriting system. It allows the
description of cell signalling pathway. In such graphs, nodes denote
proteins. Each protein has an internal state (some booleans). Proteins
have also binding sites to bind each other.

We use the abstract interpretation framework to overapproximate the set
of all reachable proteinic complexes. We use these information in order
to simplify rewriting rule systems, while preserving underlying
transition systems.

Our reachability analysis is very accurate. We give sufficient
conditions (over rewriting rule systems)  that ensure that our analysis
computes exactly the set of reachable complexes. System simplficiation
may then be seen as a program transformation that helps rewriting
system into satisfying these conditions.

These analyses are implemented in the 'Complx' tools. We will use this
tool to analyze two examples: EGF (Epidermal growth factor) and FGF
(fibroblast growth factor).

Joint work (alphabetic order): Vincent Danos, J'er^ome Feret,
Walter Fontana, Jean Krivine.
Harvard Medical School
Plectix Biosystems
'Ecole Normale Sup'erieure

*********************************************************************
Pour recevoir l'annonce par courrier electronique: 
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************