Je m'intéresse particulièrement aux liens qui existent entre la planification (comme domaine de l'intelligence artificielle) et le model-checking, avec pour objectif le développement de techniques modulaires de vérification de systèmes répartis. Une liste de mes publications est disponible ici.
Travaux en cours
Analyse paresseuse d'atteignabilité dans les systèmes répartis
En collaboration avec : Didier Lime.
Travaux de postdoctorats
De septembre 2012 à décembre 2013 j'ai travaillé à l'Université Technique de Munich (Allemagne) dans l'équipe de Javier Esparza (Chair for Foundations of Software Reliability and Theoretical Computer Science). J'ai ensuite travaillé, jusqu'en aout 2014, au LSV (Cachan France) dans l'équipe MExICo dirigée par Stefan Haar.
Calcul de résumés par dépliage de réseaux de Petri
En collaboration avec : Javier Esparza et Stefan Schwoon.
Notre objectif était de décrire exactement tous les comportements possibles d'un automate (que nous appelons interface) à l'intérieur d'un réseau d'automates. Pour cela nous calculons le produit des différents automates comme un réseau de Petri, que nous déplions, projetons sur l'interface, puis replions afin d'obtenir un automate (que nous appelons résumé) représentant les comportements de l'interface au sein du réseau. L'objectif est de trouver des conditions d'arrêt du dépliage permettant de déplier assez pour connaître totalement le comportement de l'automate qui nous intéresse (c'est-à-dire l'ensemble de ses traces), tout en assurant l'arrêt du dépliage dans tous les cas. Une approche qui peut sembler raisonnable consiste à stopper le dépliage sur les événements qui correspondent à l'interface de façon standard (c'est à dire quand ils permettent d'atteindre un marquage déjà rencontré) ainsi que sur les événements qui n'appartiennent pas à l'interface mais qui permettent d'atteindre un marquage déjà rencontré et tel qu'aucun événement de l'interface n'a été utilisé depuis ce marquage. Nous avons donné un contre-exemple à la validité de cette approche. Nous avons aussi proposé une autre approche (et montré sa validité) dans laquelle le dépliage peut être stoppé de façon temporaire sur un événement n'appartenant pas à l'interface puis repris si certains événements de l'interface ajoutés par la suite le rendent potentiellement utile. Ces travaux ont donné lieu à une publication à la conférence FSTTCS'13.
Algorithmes par passage de messages pour la vérification de systèmes répartis
En collaboration avec : Javier Esparza.
Nous avons montré que les algorithmes par passage de message étudiés pendant ma thèse pour la planification peuvent être étendus pour réaliser le model checking de propriétés locales de systèmes répartis. Nous avons notamment montré comment vérifier de propriétés de sûreté et de vivacité locales. À partir de ces résultats théoriques nous avons implanté un outil de model checking qui a ensuite été testé (et comparé à l'outil SPIN) avec succès sur deux modèles de systèmes répartis : un protocole d'exclusion mutuelle dû à Kerry Raymond et un protocole de diffusion de messages dans un réseau (Pragmatic General Multicast). Ces travaux ont donné lieu à une publication à la conférence VMCAI'14.
Calcul d'attracteurs par dépliage de réseaux de Petri
En collaboration avec : Thomas Chatain, Stefan Haar, Loïc Paulevé, et Stefan Schwoon.
Opacité et concurrence
En collaboration avec : Béatrice Bérard, Stefan Haar, John Mullins, et Stefan Schwoon.
Travaux de thèse
De septembre 2009 à septembre 2012 j'ai travaillé sur ma thèse à l'IRISA (Rennes, France) sous la direction de Éric Fabre. Durant cette période j'ai principalement travaillé sur des techniques de planification factorisée (c'est-à-dire où les problèmes sont résolus par morceaux afin d'éviter l'explosion combinatoire de leur espace d'états) minimisant le coût (en énergie par exemple) des solutions trouvées.
Algorithmes par passage de messages pour la planification
En collaboration avec : Éric Fabre, Patrik Haslum et Sylvie Thiébaux.
Nous avons montré que des algorithmes dits « par passage de messages », utilisés notamment en résolution de contraintes, peuvent être utilisés pour trouver des chemins de poids minimum dans des réseaux d'automates. Ces algorithmes permettent de calculer un résumé de chacun des automates d'un réseau (c'est-à-dire une représentation complète du comportement de cet automate au sein du réseau) par des calculs locaux (entre un automate et ses voisins). On peut ensuite, très simplement et sans backtracking, extraire de ces résumés un chemin de poids minimum de l'automate produit de tous les automates du réseau, sans avoir eu à calculer ce produit. Ces résultats trouvent leurs applications, notamment, en planification et ont été implantés sous la forme d'un outil : Distoplan, dont la dernière version a été écrite a l'aide du langage Scala. Ces travaux ont donné lieu à plusieurs publications (notamment CDC'09 et ICAPS'10) et sont regroupés dans ma thèse.
A* réparti
En collaboration avec : Éric Fabre.
L'utilisation d'algorithmes par passage de message pour la planification peut être qualifiée d'approche par le haut : à partir d'une représentation de l'ensemble des solutions locales de chaque composant, on procède par raffinements successifs pour ne garder que les solutions faisant partie d'une solution globale au problème. À la fin de ma thèse nous avons aussi travaillé sur une approche par le bas pour résoudre le même problème : une solution unique au problème global est construite par un ensemble coordonné d'agents (un par composant). Chaque agent exécute en fait une recherche locale de chemins en utilisant un algorithme proche de A*, cette recherche étant contrainte par des informations obtenues des autres agents sur leur propre recherche. Ces travaux ont donné lieu à une publication à la conférence CDC'12 et sont généralisés dans ma thèse.
Diagnostic probabiliste
En collaboration avec : Éric Fabre.
En parallèle de mes travaux de thèse nous nous sommes intéressés à la notion de diagnostique probabiliste : on souhaite, étant donné un automate probabiliste dont seules certaines actions sont observables, construire une machine d'états finis déterministe (appelée observeur) qui permette, étant donnée une séquence d'actions observées dans l'automate, de calculer la probabilité d'avoir atteint chacun des états de celui-ci. Nous avons proposé une méthode pour calculer un observeur qui soit lui même un automate probabiliste. Il existait déjà une méthode de calcul d'observeur dans ce contexte, mais en changeant la puissance du modèle : un automate avec des matrices de probabilités sur ses transitions plutôt que simplement des probabilités. Ces travaux ont donné lieu à une publication à la conférence WODES'10.