Thèse Réalisabilité des Types de Session Au-Delà des Automates Communicants H/F - Doctorat.Gouv.Fr

Établissement : Université Côte d'Azur École doctorale : STIC - Sciences et Technologies de l'Information et de la Communication Laboratoire de recherche : I3S - Informatique, Signaux et Systèmes de Sophia-Antipolis Direction de la thèse : Etienne LOZES ORCID 000000018505585X Début de la thèse : 2026-10-01 Date limite de candidature : 2026-05-03T23:59:59 Un type de session est une spécification d'un protocole d'échanges de messages
entre plusieurs agents. Plus précisément, un type global est un automate fini
dont les transitions sont étiquetées par des flèches p q : m (l'agent p envoie
à l'agent q le message m). Un type global peut être projeté sur chaque agent,
ce qui donne un type local utilisé pour vérifier que, localement, l'agent suit
le protocole. Formellement, le type local est une machine à états finis
communicante dont les transitions sont étiquetées par des actions d'envoi !m
ou de réception ?m. Un type global qui n'est pas réalisable conduit à un
système projeté qui reconnaît des Message Sequence Charts en dehors du
langage du type global, correspondant à des exécutions où les agents se sont
« décorrélés ».
Le type global est dit réalisable (ou parfois implémentable) si, lorsque tous
les agents suivent leurs types locaux, leurs interactions respectent le type
global. Plus précisément, le système projeté ne doit reconnaître que les
Message Sequence Charts du type global. De nombreux formalismes de types
de session imposent des restrictions sur les types globaux pour garantir la
réalisabilité. Très récemment, une nouvelle ligne de travaux a émergé pour
caractériser la classe des types globaux réalisables et fournir des algorithmes
et des outils pour vérifier la réalisabilité. Les types globaux constituent aussi
un cas particulier d'automates sur des alphabets partiellement commutatifs,
et leurs Message Sequence Charts sont un cas particulier de traces de
Mazurkiewicz. Zielonka a introduit un modèle d'automates (appelés, de manière
confuse, « automates asynchrones ») qui peut être utilisé pour, d'une certaine
manière, projeter un type global. Il existe des différences importantes entre
automates communicants et automates de Zielonka, ainsi qu'entre la projection
« standard » et celle connue sous le nom de « construction de Zielonka ».
Cette thèse vise à explorer de nouveaux modèles d'automates et de nouveaux
opérateurs de projection pour les types globaux, en s'intéressant à des
questions telles que la canonicité, la complétude, la décidabilité et la
complexité de la réalisabilité, etc. Sont d'un intérêt particulier des modèles
d'automates (à définir) pouvant « revenir en arrière » et annuler certaines
de leurs actions précédentes (voir par exemple un modèle réversible, ou un
modèle de résolution de conflits). D'autres modèles qu'il serait intéressant
de formaliser et d'explorer seraient des automates communicants « alternants ». Enfin, l'exploration de formes plus riches de types globaux (par
exemple avec des probabilités, ou avec des contraintes temporelles) et de leur
projection entre aussi dans le périmètre de cette proposition de thèse. Ce projet de thèse s'inscrit dans le cadre d'allocations doctorales attribuées par Université Côte d'Azur à l'issue d'une sélection. La date de début est indiquée au 1er Octobre mais une souplesse d'un mois est possible. Le financement du doctorat est soumis aux processus académiques usuels de sélection des allocations doctorales. Voir: https://webusers.i3s.unice.fr/edstic/3-2-candidater-fr.php et pour l'EUR-DS4H https://ds4h.univ-cotedazur.eu/education/phd/annual-campaign

This PhD subject is part of a doctoral grant awarded by the Université Côte d'Azur following a selection process. The start date is October 1, but can be flexible up to one month. More details on the selection process can be found on https://webusers.i3s.unice.fr/edstic/3-2-candidater-en.php and for EUR-DS4H https://ds4h.univ-cotedazur.eu/education/phd/annual-campaign
***

Le candidat devra être titulaire d'un M2 ou grade équivalent au moment du recrutement.