Description
Date depot: 1 janvier 1900
Titre: Analyse de programmes concurrents via des outils de combinatoire analytique et de théorie des ordres.
Directrice de thèse:
Michèle SORIA (LIP6)
Directeur de thèse:
Antoine GENITRINI (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Cette proposition de thèse de doctorat s’inscrit dans l’étude des structures mathématiques sous-jacentes des programmes concurrents et parallèles. Dans des travaux publiés récemment, nous avons mis en lumière un isomorphisme fondamental entre le parallélisme et l’étiquetage croissant de structures discrètes. En exploitant des techniques de combinatoire analytique, nous en avons déduit des résultats quantitatifs marquants concernant notamment le phénomène d’explosion combinatoire inhérent au parallélisme. Nous avons également développé de nouveaux algorithmes efficaces permettant la génération aléatoire uniforme d’exécutions concurrentes. Ces algorithmes peuvent être appliqués dans le cadre du model-checking statistique.
La thèse s’inscrira également dans le cadre d’une collaboration entre chercheurs provenant de différentes composantes fondamentales de l’informatique théorique :
la combinatoire et en particulier la combinatoire analytique,
la théorie des ordres partiels et les graphes dirigés acycliques,
les méthodes probabilistes en particulier la simulation par chaîne de Markov.
Objectifs de la thèse
Dans le cadre de stages de Master 2 en 2013 et 2014, nous avons étudié l’interprétation combinatoire du phénomène de la synchronisation entre processus concurrents. En comparaison de nos précédents travaux - portant essentiellement sur des structures d’arbres et leur étiquetage croissant - les opérateurs de synchronisation peuvent s’interpréter de deux façons équivalentes :
l’étiquetage non-strictement croissant de structures arborescentes,
l’étiquetage strictement croissant de graphes dirigés acycliques (DAGs)
Ceci représente un saut qualitatif important. On sait notamment que le comptage du nombre d’étiquetages croissants d’un DAG est un problème #P-complet (Brightwell et Winkler, 1991). Cela représente également un cas difficile dans le cadre de la combinatoire analytique.
L’objectif principal de la thèse proposée concerne l’intégration des différents modèles combinatoire que nous avons étudiés : étiquetage croissant pour le parallélisme (cf. AOFA 2012), étiquetage sélectif pour le non-déterminisme (cf. FSTTCS 2013) et etiquetage
non-strict pour la synchronisation.
En pratique, deux sous-problémes seront étudiés.
Le premier consistera en la caractérisation combinatoire d’un langage concurrent complet (du type CCS - Milner). Pour le moment, nos approches ont eu pour but de comprendre la combinatoire de sous-ensembles ne comportant qu’un petit nombre d’opérations. Le fait de vouloir comprendre la combinatoire d’un système global (dont certaines opérations n’ont pas encore été abordées : la récurrence par exemple) est ambitieux, mais raisonnable grâce à nos précédent travaux, notamment dans le cadre du projet PEPS “ALPACA”.
La seconde partie de la thèse portera sur le développement d’outils algorithmiques novateurs afin de pouvoir étudier les systèmes concurrents dans une approche statistique. Le but à terme est l’élaboration d’un logiciel prototype permettant de faire du model-checking statistique de modèles concurrents de grande taille. Afin d’y parvenir, deux approches complémentaires seront à étudier et comparer : la génération uniformes très efficaces via les outils de combinatoire analytique et la génération via des chaînes de Markov de Monte Carlo (basée sur des travaux de M. Huber).
Doctorant.e: Dien Matthieu