Réalisabilité des types de session au-delà des automates communicants // multiparty session types: realisability beyond communicating automata

Topic description

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

A session type is a specification of a protocol of message exchanges
between several agents. More precisely, a global type is a finite automaton
whose transitions are labeled by arrows p → q : m (agent p sends to agent q the message m). A global type may be projected on each agent, leading to a local type that is used to check that, locally, the agent follows the protocol. Formally, the local type is a communicating finite state machine whose transitions are labeled by send actions !m or receive actions ?m. A global type that is not realisable leads to a projected system that recognizes Message Sequence Charts that are outside the language of the global type, corresponding to executions where the agents have ”decorrelated”.
The global type is said to be realisable (or sometimes, implementable)
if, when all agents follow their local types, their interactions obey with the global type. More precisely, the projected system should recognize only the Message Sequence Charts of the global type. Many session type formalisms impose some restrictions on the global types to ensure realisability. Quite recently, a new line of work has emerged to characterize the class of realisable global types, and to provide algorithms and tools to check realisability. Global types are also a special case of automata on partially commutative alphabets, and their Message Sequence Charts are a special case of Mazurkiewicz traces. Zielonka introduced a model of automata
(confusingly called ”asynchronous automata”) that can be used to somehow
project a global type. There are important differences between communicating automata and Zielonka automata, and between the ”standard” projection and the one known as ”Zielonka construction”. This Phd aims to explore new automata models and new projection operators for global types, looking at questions like canonicity, completeness, decidability and complexity of realisability, etc. Of particular interests are models of automata (to be defined) that can ”backtrack” and cancel some of their pre-
vious actions (see for instance a reversible model, or a conflict-resoluting
model). Other models that would be interesting to formalise and explore
would be ”alternating” communicating automata. Finally,
exploring richer forms of global types (for instance, with probabilities, or with
timings) and their projection also fits in the scope of this Phd proposal.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/10/

Funding category

Funding further details

Contrat doctoral EDSTIC-DS4H