logo inria

RR-4350 - On the Expressiveness of Pure Safe Ambients

-----------------------
Zimmer, Pascal
Rapport de recherche de l'INRIA - Sophia Antipolis , Equipe : MIMOSA
54 pages - Janvier 2002 - Document en anglais
Titre français : Etude de l'Expressivité des Ambients Mobiles Purs
-----------------------
Abstract : We consider the Pure Safe Ambient Calculus, which is Levi and Sangiorgi's Safe Ambient Calculus (a variant of Cardelli and Gordon's Mobile Ambient Calculus) restricted to its mobility primitives, and we focus on its expressiv- e power. Since it has no form of communication or substitution, we show how these notions can be simulated by mobility and modifications in the hierarchical structure of ambients. As a main result, we use these techniques to design an encoding of the synchronous pi-calculus into pure ambients, and we study its correctness, thus showing that pure ambients are as expressive as the pi-calculus. In order to simplify the proof and give an intuitive understanding of the encoding, we design an intermediate language: the pi-calculus with Explicit Substitutions and Channels, which is an extension of the pi-calculus in which communication and substitution are broken into simpler steps, and we show that is has the same expressive power as the pi-calculus.

Résumé : Nous étudions le Calcul des Ambients Purs, qui correspond au Calcul des Ambients de Cardelli et Gordon restreint aux seules primitives de mouvement, et nous nous intéressons plus particulièrement à sa puissance expressive. Etant donné qu'il ne possède aucune forme de communication ni de substitution, nous montrons comment ces notions peuvent être simulées par la mobilité et des modifications de la structure hiérarchique des ambients. Comme résultat principal, nous utilisons ces techniques pour construire un encodage du pi-calcul synchrone dans les ambients purs et nous étudions sa correction, prouvant par conséquent que les ambients purs sont aussi expressif- s que le pi-calcul. Afin de simplifier la preuve et de faciliter la compréhens- ion intuitive de l'encodage, nous introduisons un langage intermédiaire: le pi-calcul avec Substitutions et Canaux Explicites, qui est une extension du pi-calcul dans laquelle la communication et la substitution sont décomposées en étapes plus élémentaires, et nous montrons qu'il possède aussi la même puissance expressive que le pi-calcul.
-----------------------
Key-Words : MOBILE AMBIENTS / SAFE AMBIENTS / PI-CALCULUS / CONCURRENT AND MOBILE SYSTEMS / EXPRESSIVENESS
Mots-clés : AMBIENTS MOBILES / SAFE AMBIENTS / PI-CALCUL / SYSTÈMES CONCURRENTS ET MOBILES / EXPRESSIVITÉ
-----------------------