Stage de Master - Vérification de propriétés dynamiques pour un modèle hybride de contrôle d’une épidémie

Niveau : Master 2

Période : Mars - Aout 2024

L’objectif principal de ce stage consiste à étudier les propriétés d’un modèle de dynamique épidémiologique, déterminé par un processus de décision markovien. Ce modèle hybride est obtenu par couplage d’un processus continu déterministe avec un processus discret probabiliste, et doit reproduire la juxtaposition d’une dynamique virale continue avec une dynamique humaine de prise de décisions. En plus des propriétés usuelles telles que l’adéquation du modèle aux données d’observation, l’accessibilité et l’invariance des équilibres du modèle, on s’intéressera particulièrement aux propriétés dynamiques telles que la stabilité et la périodicité des trajectoires. Les méthodes de vérification utilisées seront de nature numérique et reposeront sur un traitement statistique d’un ensemble de traces du modèle produites par simulation numérique. Suivant l’avancée du travail, des méthodes de vérification symboliques associées à une procédure algorithmique pourront également être étudiées.

Guillaume Cantin (guillaume.cantin@ls2n.fr) ; Morgan Magnin (morgan.magnin@ls2n.fr) ; Benoît Delahaye (benoit.delahaye@ls2n.fr)