Modèles logiques pour la représentation formelle des systèmes vivants

22-23 juin 2017, campus CNRS de Gif-sur-Yvette

Programme

Ces journées ont pour but de donner un aperçu des recherches actuelles en France sur la représentation formelle et le raisonnement automatique appliqués à l'étude des systèmes vivants, en particulier menées par les participants au GT BIOSS et au pré-GDR IA, et de décider la création éventuelle d'un GT commun sur ce thème.

Avec le soutien du preGDR IA, GdR BiM, GT BIOSS, et GT TheoBioR du labex Digicosme

Inscription

Les inscriptions sont closes, si vous souhaitez toute de même assister aux présentations, merci de contacter les organisateurs.

Programme

Jeudi 22 Juin, 13h30 - 18h30

Salle 2, bâtiment 31

13h30 - 14h00Accueil et mot d'introduction
14h00 - 15h00Keynote François Fages (Inria)
En quête du logiciel du vivant: succès et difficultés du paradigme de la vérification de programmes en biologie cellulaire
15h00 - 15h20 Exposé Laurent Trilling (Univ Grenoble)
Modélisation déclarative de réseaux de régulation génique. Apport de la programmation logique « non monotone »
15h20 - 15h50Pause café
15h50 - 16h10 Exposé Morgan Magnin (École Centrale Nantes)
Enjeux de l'apprentissage de modèles dynamiques des réseaux biologiques par la programmation logique
16h10 - 16h30 Exposé Anne Siegel (CNRS)
Raisonner sur des abstractions et invariants de systèmes dynamiques en biologie avec ASP
16h30 - 16h50 Exposé Céline Rouveirol (Univ Paris Nord)
Découverte dans les réseaux biologiques hétérogènes : l'expérience Adalab
16h50 - 17h10Pause café
17h10 - 17h30 Exposé Béatrice Duval (Univ Angers)
Analyse différentielle de réseaux
17h30 - 17h50 Exposé Philippe Dague (Univ Paris-Sud)
Analyse de réseaux métaboliques en présence de contraintes biologiques : approches géométriques, combinatoires et logiques
17h50 - 18h30Discussions

Vendredi 23 Juin, 9h00 - 15h30

Salle 2, bâtiment 31

9h30 - 9h50 Expose Andrei Doncescu (Univ Paul Sabatier Toulouse)
Quel type de modélisation pour des interactions entre composants biologiques ?
9h50 - 10h50Keynote Pierre Siegel (Univ Aix-Marseille)
Logiques non-monotones pour les réseaux de gênes et les systèmes dynamiques booléens
10h50 - 11h20Pause café
11h20 - 11h40 Exposé Joëlle Despeyroux (Inria)
Towards a Logical Framework for Systems Biology
11h40 - 12h00 Exposé Loïc Paulevé (CNRS)
Approximations de problèmes PSPACE en SAT pour la reprogrammation cellulaire
12h00 - 12h20 Exposé Franck Delaplace (Univ Evry)
Abduction based drug target discovery using boolean control network
12h30 - 14h00Déjeuner
14h00 - 15h30Discussions sur le lien entre GT BIOSS et preGDR IA/biologie
Présentations
Philippe Dague (LRI, Univ Paris-Sud)
Analyse de réseaux métaboliques en présence de contraintes biologiques : approches géométriques, combinatoires et logiques
Après un rappel de l’état de l’art concernant l’analyse des réseaux métaboliques en mode stationnaire, fondée sur l’énumération des modes élémentaires de flux (efms), qui sont les solutions de support minimal caractérisées comme les rayons extrémaux du cône convexe polyédral P de toutes les solutions et en constituent un système générateur, et de la méthode de double description (DD) à l’œuvre dans la majorité des outils de calcul de ces efms, et la double constatation que ces outils ne passent pas à l’échelle du génome et que la plupart des efms calculés ne sont pas biologiquement réalistes, je montrerai comment prendre en compte dans leur définition et leur calcul plus de contraintes biologiques que la seule stoichiométrie et irréversibilité de réactions : contraintes thermodynamiques, cinétiques et de régulation génique. Je présenterai un cadre général de prise en compte de contraintes monotones par rapport au support (dont les contraintes thermodynamiques et cinétiques sont un cas particulier), fournirai la structure géométrique de l’espace des solutions comme union de cônes convexes qui sont des faces de P et montrerai comment intégrer ces contraintes au sein de la méthode de DD. Pour ce qui est des contraintes booléennes de régulation, qui ne sont pas monotones par rapport au support, je montrerai que les solutions sont encore des unions de cônes convexes inclus dans des faces de P, mais qui ne sont plus topologiquement fermés. J’étendrai dans ce cas le concept d’efms en montrant que solutions minimales, indécomposables et génératrices ne se confondent plus et que leur calcul ne s’intègre pas dans la méthode de DD. Je montrerai les résultats obtenus par une approche complètement différente, fondée sur l’utilisation d’un solveur de Satisfaisabilité Modulo Théories (SMT).
SLIDES
Franck Delaplace (IBSIC, Univ Evry)
Abduction based drug target discovery using boolean control network
SLIDES
Joëlle Despeyroux (Inria Sophia Antipolis)
Towards a Logical Framework for Systems Biology
We advocates here the use of (mathematical) logic for systems biology, as a unified framework well suited for both modeling the dynamic behaviour of biological systems, expressing properties of them, and verifying these properties. The potential candidate logics should have a traditional proof theoretic pedigree (including a sequent calculus presentation enjoying cut-elimination and focusing), and should come with (certified) proof tools. Beyond providing a reliable framework, this allows the adequate encodings of our biological systems. We have up to now two candidate logics; both are modal extensions of linear logic. The examples we have considered so far are very simple ones - coming with completely formal (interactive) proofs in Coq. Future works includes using automatic provers, which would extend existing automatic provers for linear logic. This should enable us to specify and study more realistic examples in systems biology and biomedicine.
SLIDES
Andrei Doncescu (LAAS, Univ Paul Sabatier Toulouse)
Quel type de modélisation pour des interactions entre composants biologiques ?
SLIDES
Béatrice Duval (LERIA, Univ Angers)
Analyse différentielle de réseaux
SLIDES
François Fages (Inria Saclay-Île-de-France)
En quête du logiciel du vivant: succès et difficultés du paradigme de la vérification de programmes en biologie cellulaire
Dans cet exposé je brosserai un tableau général des méthodes formelles issues de l’informatique appliquées à l’analyse/synthèse des processus biochimiques dans la cellule, des réussites obtenues dans ce domaine, des difficultés liées à l’importance des calculs biochimiques continus, et de perspectives inattendues sur l'apprentissage automatique et l’évolution.
SLIDES
Morgan Magnin (LS2N, École Centrale Nantes)
Enjeux de l'apprentissage de modèles dynamiques des réseaux biologiques par la programmation logique
Au cours des dix dernières années, nous nous sommes intéressés à la conception de méthodes efficace d'analyse de la dynamique chronologique et chronométrique de réseaux de régulation biologiques de grande taille. Mais avant même de pouvoir analyser, il faut disposer de modèles en entrée. C'est la raison pour laquelle, devant l'essor des données de séries temporelles d'expression génétique, nous développons désormais des méthodes d'apprentissage de modèles basées sur la programmation logique. Dans cet exposé, j'évoquerai quelques-uns des verrous que nous attaquons.
SLIDES
Loïc Paulevé (CNRS, LRI)
Approximations de problèmes PSPACE en SAT pour la reprogrammation cellulaire
SLIDES
Céline Rouveirol (LIPN, Univ Paris Nord)
Découverte dans les réseaux biologiques hétérogènes : l'expérience Adalab
SLIDES
Anne Siegel (CNRS, IRISA, Rennes)
Raisonner sur des abstractions et invariants de systèmes dynamiques en biologie avec ASP
SLIDES
Pierre Siegel (LIF, Univ Aix-Marseille)
Logiques non-monotones pour les réseaux de gênes et les systèmes dynamiques booléens
SLIDES
Laurent Trilling (TIMC-IMAG, Univ Grenoble)
Modélisation déclarative de réseaux de régulation génique. Apport de la programmation logique « non monotone »
A. Rocca, E. Fanchon, L. Trilling
Nous nous intéressons principalement aux réseaux logiques proposés par René Thomas. Par approche déclarative, nous entendons : représentation de toutes les données biologiques disponibles (sur la structure ou la dynamique), sous forme d'axiomes logiques et obtention sous forme intensionelle des réseaux de Thomas cohérents avec ces données. Pour ce faire, nous nous appuyons sur la technologie de programmation logique ASP (Answer Set Programming), basée sur une logique non monotone n'admettant que certains modèles logiques, dits stables: intuitivement, ne sont vrais que les atomes prouvables. Nous soulignerons les choix de modélisation et en mettrons en évidence les avantages de l'approche, comme la réparation automatique d’inconsistance et l'apprentissage de toutes les propriétés (théorèmes) avec une formulation fixée des réseaux retenus. Deux avantages généraux d'ASP sont reconnus : traitement des données incomplètes et pouvoir de déduction augmenté. Nous nous focaliserons plutôt sur : 1) l'utilisation de défauts pour spécifier la réparation d'inconsistance, 2) la méthodologie de construction d'une conjonction de défauts originale en particulier pour exprimer les composition d'interactions généralement vraies, 3) la spécification opérationnelle de formules CTL générales, en particulier du type AF (expression de propriétés de comportement exhaustives), en prenant appui sur la minimalité des modèles stables. Nous terminerons en évoquant des projets en cours.
SLIDES
Participants

Participants

  • Belaïd Benhamou (Univ Aix-Marseille)
  • Célia Biane (IBISC, Univ Evry)
  • Philippe Dague (LRI, Univ Paris-Sud)
  • Franck Delaplace (IBISC, Univ Evry)
  • Bruno Delord (UPMC)
  • Joëlle Despeyroux (Inria Sophia Antipolis)
  • Andrei Doncescu (LAAS CNRS)
  • Béatrice Duval (LERIA, Univ Angers)
  • François Fages (Inria Saclay-Île-de-France)
  • Éric Fanchon (CNRS)
  • Christine Froidevaux (LRI, Univ Paris-Sud)
  • Adrien Husson (Univ Paris Diderot)
  • Tarek Khaled (Univ Aix-Marseille)
  • Sébastien Konieczny (CNRS, CRIL)
  • Cédric Lhoussaine (Univ Lille)
  • Yue Ma (LRI, Univ Paris-Sud)
  • Morgan Magnin (LS2N, École Centrale de Nantes)
  • Englebert Mephu Nguifo (LIMOS, Univ Clermont Auvergne)
  • Loïc Paulevé (CNRS, LRI)
  • Fabrice Popineau (Supelec, LRI)
  • Élisabeth Rémy (CNRS)
  • Céline Rouveirol (LIPN)
  • Anne Siegel (CNRS, IRISA)
  • Pierre Siegel (LIF, Univ Aix-Marseille)
  • Laurent Simon (LABRI, Univ Bordeaux)
  • Laurent Trilling (TIMC-IMAG, Univ Grenoble)
  • Lucas Venturini (IBISC, Univ Evry)
  • Chai Xinwei (LS2N, Nantes)
Accès

Transports en commun

Le campus du CNRS est accessible en 15min à pied depuis la gare de Gif-sur-Yvette du RER B. Les journées se déroulent dans la salle 2 du bâtiment 31 (centre de formation)


Depuis la gare de Massy TGV

RER B direction Saint-Rémy-lès-Chevreuse (fréquence: tous les 15min), arrêt Gif-sur-Yvette; environ 15min de trajet.

Depuis la gare de Lyon

RER A direction Ouest, puis RER B direction Sud Saint-Rémy-lès-Chevreuse (fréquence: tous les 15min), arrêt Gif-sur-Yvette; environ 60min de trajet.

Depuis l'aéroport d'Orly

Orly val, puis RER B direction Saint-Rémy-lès-Chevreuse (fréquence: tous les 15min), arrêt Gif-sur-Yvette; environ 40min de trajet.

En voiture

Parking devant l'entrée du campus CNRS
Coordonnées GPS: 48.7033, 2.1324

Contact

Organisateurs: Philippe Dague et Loïc Paulevé; prenom.nom@lri.fr