Description
Date depot: 1 janvier 1900
Titre: A Denotational Semantics for Mobility
Directrice de thèse:
Amal EL FALLAH SEGHROUCHNI (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
La sémantique des systèmes concurrents a été largement étudiée. Même si plusieurs pistes ont été explorées, il y a deux écoles de pensée en la matière. La première promeut le pi-calcul, une algèbre de processus définie en étendant son ancêtre CCS. Son point de vue sémantique est opérationnel, étant donné que les processus sont représentés comme des systèmes de transitions étiquetées. Son avantage principale est qu'il permet de représenter la mobilité, c'est-à-dire la capacité des processus à changer de voisins, de façon intuitive. Ceci est possible en permettant à la portée des canaux de varier. La seconde approche repose sur CSP, une algèbre de processus qui est construite du point de vue dénotationnel, en tant qu'un langage concurrent à passage de valeurs dont les processus sont représentés dans un système de traces ensemblistes qui a été étendu année après année. Même si CSP ne gère pas nativement la mobilité, il a été récemment montré qu'il est suffisamment expressif pour encoder le pi-calcul.
Le but principal de cette thèse était et est toujours de construire un pont entre les deux mondes, en apportant une algèbre de processus qui soit à la fois intégralement mobile comme le pi-calcul, avec toute l'expressivité de la portée dynamique des canaux, mais aussi intégralement dénotationnelle comme CSP, avec une dénotation ensembliste définie pour chaque processus en lieu et place d'une caractérisation opérationnelle. Afin de conserver l'expressivité complète du pi-calcul, une partie de sa syntaxe et de ses constructions ont dû être conservées, spécifiquement son concept de restriction de portée qui, avec la possibilité d'envoyer des canaux à portée réduite à travers des canaux publics, permet de rendre la portée des canaux intégralement dynamique. Ces constructions, qui sont nécessaires pour la véritable mobilité, ne sont toutefois pas compatibles avec le concept d'échecs et de divergences hérité de CSP, dans la mesure où il impose qu'un nom de canal ait le même sens d'un bout à l'autre d'une trace d'exécution. Ceci a imposé de repenser le concept de traces étendues et d'introduire des localisations afin de lier chaque observation au potentiel du processus de permettre de nouvelles interactions à ce niveau, non pas à travers des ensembles de refus mais plutôt en utilisant une identification spatiale unique du nœud correspondant dans la structure de branchement du processus.
Les contributions de la thèse sont les suivantes. D'abord, une algèbre de processus qui est d'une certaine façon un hybride entre le pi-calcul et CSP, et est à la fois dénotationnelle, compositionnelle et mobile est introduite. Elle est dénotationnelle parce que toute expression de processus peut être traduite en un modèle ensembliste sans perte d'information. Elle est compositionnelle parce que ces modèles peuvent être combinés sans tenir compte du contexte, et une relation d'équivalence indépendante du contexte a pu être conçue. Elle est mobile parce qu'elle partage la totalité des propriétés mobiles du pi-calcul, non seulement le passage de canaux mais aussi l'extrusion de portée. Ensuite, une sémantique axiomatique est également fournie, et il est prouvé qu'elle est correcte et complète pour la partie finie du langage. En raison de ses propriétés, l'algèbre de processus se comporte avec élégance vis-à-vis de l'opérateur de mismatch, ce qui n'est pas une évidence pour de nombreuses versions du pi-calcul. De plus, une théorie du raffinement est proposée pour le langage. Même si elle reste perfectible, c'est inédit dans le monde de la mobilité. Enfin, une logique dénotationnelle a été conçue en suivant en cela l'exemple de CSP.
Doctorant.e: Bialkiewicz Joel-Alexis