logo EDITE Sujets de doctorat

Analyse de programmes concurrents via des outils de combinatoire analytique et de théorie des ordres.

Sujet proposé par
Directeur de thèse:
Encadré par
Doctorant: Matthieu DIEN
Unité de recherche UMR 7606 Laboratoire d'informatique de Paris 6

Domaine: Sciences et technologies de l'information et de la communication

Projet

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).

Enjeux

Cette thèse représente le point culminant de notre étude des langages concurrents sous l'angle de la combinatoire. Le premier défi scientifique relevé concerne le rapprochement entre les techniques de génération aléatoire issues de la combinatoire analytique (méthode récursive, Boltzman, etc.) et les techniques à base de chaînes de Markov par couplage depuis le passé. Le deuxième défi scientifique est moins directement technique: comment analyser des systèmes concurrents de grande taille, alors que l'on sait qu'ils sont source d'explosion combinatoire ? Nous pensons que l'analyse statistique (statistical model-checking), développée dans le cadre de cette thèse, et basée sur nos modèles combinatoires représente une réponse pertinente à cette question difficile.

Ouverture à l'international

Le sujet s’inscrit naturellement au sein de deux communautés que sont l’analyse d’algorithmes et la théorie de la concurrence. Ce travail de thèse repose sur des publications dans des conférences et revues internationales couvrant les deux domaines : AOFA 2012 et FSTTCS 2013. Nous sommes donc confiants quant à la haute compétitivité de cette thèse de doctorat dans un contexte international.

Remarques additionnelles

Bibliographie

O. Bodini, A. Genitrini et F. Peschanski : Enumeration and Random Generation of Concurrent Computations, DMTCS AofA'12 proceedings, p. 83-96, 2012.

The combinatorics of Non-determinism, FSTTCS’13 proceedings, p. 425-436, 2013.

G. Brightwell et P. Winkler : Counting Linear Extensions is #P-Complete, STOC, p. 175-181, 1991.

M. Huber : Fast Perfect Sampling From Linear Extensions, Discrete Mathematics vol 306(4), p. 420-428, 2006