BIALKIEWICZ Joël-Alexis

Docteur
Équipe : APR
Date de départ : 30/09/2010
Direction de recherche : Amal EL FALLAH SEGHROUCHNI
Co-encadrement : PESCHANSKI Frédéric

Vers une sémantique dénotationnelle pour la mobilité

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. Ce dernier but n’a pas été totalement atteint. 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 une variant du pi-calcul qui s’inspire de CSP, et est à la fois compositionnelle et mobile est introduite. 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. Malgré ses faiblesses, elle constitue un pas non négligeable vers un modèle dénotationnel. 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 a été conçue en suivant en cela l'exemple de CSP.
Soutenance : 10/01/2011 - 10h
Membres du jury :
Mme EL FALLAH SEGHROUCHNI Amal
M. ROSCOE Andrew William [Rapporteur]
M. GOLDSMITH Michael [Rapporteur]
Mme CASTELLANI Ilaria
M. HIRSCHKOFF Daniel
Mme BERARD Béatrice
M. PESCHANSKI Frédéric Encadrant

Publications 2009-2011

  • 2011
  • 2009
    • J.‑A. Bialkiewicz, F. Peschanski : “A Denotational Study of Mobility”, Communicating Process Architectures, vol. 67, Concurrent Systems Engineering Series, Eindhoven, Netherlands, pp. 239-261, (IOS Press), (ISBN: 978-1-60750-065-0) (2009)
    • J.‑A. Bialkiewicz, F. Peschanski : “Logic for Mobility: A Denotational Approach”, Second International Workshop on Logics for Agents and Mobility, Los Angeles, California, USA, pp. 44-59, (Durham University) (2009)
    • F. Peschanski, J.‑A. Bialkiewicz : “Modelling and Verifying Mobile Systems Using Pi-Graphs”, 35th International Conference on Current Trends in Theory and Practice of Computer Science (Sofsem 2009), vol. 5404, Lecture Notes in Computer Science, Špindlerův Mlýn, Czech Republic, pp. 437-442, (Springer) (2009)
 Mentions légales
Carte du site |