CNRS

Parcours

Nathanaël Fijalkow, 06/03 et 06/04

Méthodes formelles pour la vérification,
ouverture vers science des données

Sept. 2012 - Oct. 2015 : Thèse cotutelle Paris 7 - Varsovie (Colcombet / Bojańczyk)
Nov. 2015 - Juill. 2016 : Post-doctorat Oxford (Ouaknine / Worrell)
Août 2016 - Déc. 2016 : Chercheur invité Simons Institute Berkeley (Panangaden)
Jan. 2017 - ? : Chercheur Alan Turing Institute of Data Science Londres

Implication dans la communauté scientifique :

Publications : conférences (LICS, ICALP, STACS, ...), journaux (LMCS, ToCL, TCS,...)
Exposés invités : AutoMathA, Cassting
Développement logiciel : ACME, Stamina, Flides
Encadrement d'étudiants : Paris, Varsovie, Oxford, Londres
Projets de recherche : ANR (FREC, STOCH-MC), ERC (SOSNA, GALE, AVS-ISS)
Organisation d'évènements scientifiques : conférences (Highlights), séminaires (Paris, Oxford, Berkeley), workshops (GT-ALGA)

Diffusion scientifique :

Responsable de projets Animath (Kosovo, Laos)
Articles de vulgarisation (RMS)

Recherche

Domaine de recherche : méthodes formelles (vérification, synthèse), ouverture vers science des données

Modèles : automates, jeux, logiques, systèmes dynamiques

Outils : probabilités, complexité, algèbre, topologie, théorie des modèles

Un résultat

La théorie prostochastique

Approche profinie pour l'étude des systèmes stochastiques

Les automates probabilistes

Rabin, 1963

$$\mathbb{P}(\text{train train predict}) = 0.4 \cdot 0.6 \cdot 1\ +\ 0.6 \cdot 0.45 \cdot 1$$

Un automate probabiliste induit $\mathbb{P} : A^* \to [0,1]$

Objectif : déterminer algorithmiquement les propriétés de $\mathbb{P}$

Le problème de la valeur 1

Pas de séquence d'actions pour atteindre l'état vert avec probabilité $1$
Pour tout $\varepsilon > 0$, il existe une séquence d'actions pour atteindre l'état vert avec probabilité $1 - \varepsilon$

Problème de la valeur $1$ :
Entrée : Un automate probabiliste

Sortie : Existe-t-il une suite de mots $(u_n)_{n \in \mathbb{N}}$ tel que $\lim_n \mathbb{P}(u_n) = 1$?

Contexte

L'algorithme du monoïde de Markov

Implantation :

ACME : F. & Kuperberg
Stamina : F., Gimbert, Kelmendi & Kuperberg

Théorie prostochastique

Théorème (STACS'16, Theoretical Computer Science'17)

L'algorithme du monoïde de Markov répond OUI
si, et seulement si,
il existe une suite polynomiale $(u_n)_{n \in \mathbb{N}}$ tel que $\lim_n \mathbb{P}(u_n) = 1$

La suite $((a^n b)^n)_{n \in \mathbb{N}}$ est polynomiale
La suite $((a^n b)^{2^n})_{n \in \mathbb{N}}$ ne l'est pas

Trouver le bon langage de preuve : développement de la théorie prostochastique, pour décrire topologiquement les comportements limites des automates probabilistes

Le monoïde prostochastique libre

Théorème

$\mathbb{P} A^*$ est le complété de $A^*$, c'est un monoïde compact
Toute suite de mots est interprétable dans $\mathbb{P} A^*$
Le problème de la valeur $1$ est équivalent au problème du vide dans $\mathbb{P} A^*$
La classe des suites polynomiales forme une structure algébrique (monoïde de stabilisation)

Projet

Incertitude pour les systèmes stochastiques

Robustesse

Illustration : algorithme randomisé

Pièce biaisée : $\mathbb{P}(\text{pile}) = x$, $\mathbb{P}(\text{face}) = 1 - x$

Algorithme de von Neumann : deux lancers

même résultat : on recommence
résultats différents : premier lancer

Simule une pièce équilibrée !
Question : dépendance (robustesse) en $x$ ?

Deux axes :

Notion de distance entre systèmes stochastiques
Notion de confiance (liens avec l'apprentissage et les statistiques)

Simulation
en ligne

Rabin, 1963 : comment simuler un automate probabiliste ?
Objectif : construire un algorithme en ligne pour déterminer $\mathbb{P}(w) \ge .65$

Karp, 1967 : combien d’espace est nécessaire pour vérifier une propriété en ligne ? Lié à la précision

Deux axes :

Classification des automates probabilistes
Méthodes de bornes inférieures (liens avec la complexité)

Vœux d'affectation

Affectation dans un laboratoire d'informatique (concours 06/03)

LaBRI, Bordeaux, équipe Méthodes Formelles

Systèmes probabilistes : Hugo Gimbert (ANR Stoch-MC),
Data Science (streaming, bases de données) : Olivier Gauwin, Gabriele Puppis (ANR ExStream),
Vérification : Jérôme Leroux, Anca Muscholl, Thomas Place, Igor Walukiewicz, Marc Zeitoun

IRISA, Rennes, équipe SUMO

Systèmes probabilistes : Nathalie Bertrand, Blaise Genest, Ocan Sankur (ANR Stoch-MC),
Théorie du contrôle : Eric Fabre, Hervé Marchand,
Vérification : Sophie Pinchinat (équipe Logica)

Affectation dans un laboratoire de mathématiques (concours 06/04)

J.A. Dieudonné, Mathématiques et Interactions, Nice

Deux équipes :

Algèbre, Topologie et Géométrie : Sorin Dumitrescu, François-Xavier Dehon
- Espaces profinis : théorie prostochastique (STACS'16,TCS'17)
- Théorie des nombres algébriques : problème de l'orbite de Kannan-Lipton (STACS'17), complexité en ligne des nombres premiers (soumis)
Probabilités et Statistiques : Raphaël Chetrite, Patricia Reynaud-Bouret
- Notions de confiance : distance entre systèmes stochastiques (projet)
- Théorèmes d'ergodicité : comportements limites des automates probabilistes (LICS'12, LMCS'15)
- Apprentissage : apprentissage d'automates probabilistes

Présentation produite avec Flides

HTML5 et Javascript

Navigation :

Fléche droite ou bas : suivant
Fléche gauche ou haut : précédent
Barre d'espace : animation
Entrée : afficher tout le contenu d'un transparent
Shift : vue globale
Retour arrière : initialisation
Clic gauche : aller au transparent