Méthodes formelles pour la modélisation discrète

Code de l'ECUE : SMESV06

Ce cours est proposé dans 0 UE

Structure

EUR LIFE

Domaine disciplinaire

Informatique , Biologie cellulaire , Biologie des populations et écologie

Lieu d'enseignement

Campus Valrose

Niveau du cours

Master 1 , Master 2

Semestre

Semestre impair

Langue

Anglais

PRESENTATION

Objectifs : Ce cours donne aux étudiants la capacité de concevoir des modèles discrets bien adaptés à la question biologique abordée et d’appliquer des méthodes formelles pour les analyser (logique formelle). Il permet d'avoir une vision critique des causalités supposées des phénotypes observés, d'affiner les approches de modélisation en fonction des capacités d'observation expérimentale disponibles, et enfin de proposer des modèles prédictifs suggérant des stratégies expérimentales pour valider des hypothèses biologiques.
Contenu :
- Introduction à la théorie de René Thomas, formalisme avec multiplexes, exemples (3h)
- Compatibilité de la modélisation discrète avec la modélisation différentielle par morceaux, exemples (3h)
- Conditions de Snoussi et identifications de paramètres, théorèmes fondamentaux sur les boucles de rétroaction, états caractéristiques, exemples (3h)
- Logique temporelle et model-checking, méthode d’identification des paramètres assistée par ordinateur, exemples (3h30)

- Logique de Hoare « génétiquement modifiée » appliquée aux réseaux de régulation, extraction de contraintes sur les paramètres, exemples (3h30)

Responsable(s) du cours

Gilles Bernot , Jean-Paul Comet

Présentiel

8h de cours magistral
8h de travaux dirigés

PREREQUIS

Avant le début du cours, je dois ...

Quelques notions de base sur les réseaux de régulation biologiques

OBJECTIFS

A la fin de ce cours, je devrais être capable de...

concevoir des modèles discrets bien adaptés à la question biologique abordée
proposer des modèles prédictifs suggérant des stratégies expérimentales pour valider des hypothèses biologiques
appliquer des méthodes formelles pour les analyser (logique formelle)

CONTENU

- Introduction à la théorie de René Thomas, formalisme avec multiplexes, exemples (3h)

Aucune description
- Compatibilité de la modélisation discrète avec la modélisation différentielle par morceaux

exemples (3h)
- Conditions de Snoussi et identifications de paramètres, théorèmes fondamentaux sur les boucles de rétroaction, états caractéristiques

exemples (3h)
- Logique temporelle et model-checking, méthode d’identification des paramètres assistée par ordinateur,

exemples (3h30)
- Logique de Hoare « génétiquement modifiée » appliquée aux réseaux de régulation, extraction de contraintes sur les paramètres

exemples (3h30)
Evaluation

Modalités du contrôle des connaissances :
- Session 1 : un examen de 2h.
- Session de rattrapage : un examen oral ou écrit.

Accéder au Syllabus complet (Authentification requise)

Important

Ce syllabus n’a aucune valeur contractuelle. Son contenu est susceptible d’évoluer en cours d’année : soyez attentifs aux dernières modifications.