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

ECUE's code : SMESV06

Belong to 0 UE

Structure

EUR LIFE

Disciplinary domain

Informatique , Biologie cellulaire , Biologie des populations et écologie

Campus

Campus Valrose

Course's level

Master 1 , Master 2

Semester

Semestre impair

Language

Anglais

PRESENTATION

Objectives: This course gives students the ability to design discrete models well suited to the biological question being addressed, and to apply formal methods to analyze them (formal logic). It provides a critical view of the supposed causalities of observed phenotypes, refines modeling approaches according to available experimental observation capabilities, and finally proposes predictive models suggesting experimental strategies to validate biological hypotheses.

Contents :
- Introduction to René Thomas's theory, formalism with multiplexes, examples (3h)
- Compatibility of discrete modeling with piecewise differential modeling, examples (3h)
- Snoussi conditions and parameter identifications, fundamental theorems on feedback loops, characteristic states, examples (3h)
- Temporal logic and model-checking, computer-aided parameter identification methods, examples (3h30)

- Genetically modified” Hoare logic applied to control networks, extraction of constraints on parameters, examples (3h30)

Course's manager(s)

Gilles Bernot , Jean-Paul Comet

In class

8h of lectures
8h of directed studies

PREREQUISITES

Before the start of the course, I must ...

A few basic notions about biological control networks

OBJECTIVES

By the end of this course, I should be able to...

design discrete models that are well suited to the biological question at hand
propose predictive models suggesting experimental strategies to validate biological hypotheses
apply formal methods to analyze them (formal logic)

CONTENT

- Introduction to René Thomas theory, multiplex formalism, examples (3h)

No description
- Compatibility of discrete modeling with piecewise differential modeling

examples (3h)
- Snoussi conditions and parameter identifications, fundamental feedback loop theorems, characteristic states

examples (3h)
- Time logic and model-checking, a computer-aided method for identifying parameters,

examples (3h30)
- Genetically modified” Hoare logic applied to control networks, extraction of constraints on parameters

examples (3h30)
Evaluation

Assessment of knowledge :
- Session 1: a 2-hour examination.
- Make-up session: an oral or written exam.

Access to complete Syllabus (Authentification required)

Important

This syllabus has no contractual value. Its content is subject to change throughout this year: be aware to the last updates