Hostname: page-component-6898cfcb55-th4rj Total loading time: 0 Render date: 2026-11-11T21:30:22.692Z Has data issue: false hasContentIssue false

On the expressiveness of π-calculus for encoding mobile ambients

Published online by Cambridge University Press:  22 September 2016

LINDA BRODO*
Affiliation:
Dipartimento di Scienze Politiche, Scienze della Comunicazione e Ingegneria, dell'Informazione, Università degli Studi di Sassari, viale Mancini, 5 - 07100 - Sassari, Italia Email: brodo@uniss.it
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We investigate the expressiveness of two classical distributed paradigms by defining the first encoding of the pure mobile ambient calculus into the synchronous π-calculus. Our encoding, whose correctness has been proved by relying on the notion of operational correspondence, shows how the hierarchical ambient structure can be reformulated within a flat channel interconnection amongst independent processes, without centralised control. To easily handle the computation for simulating a capability, we introduce the notions of simulating trace (representing the computation that a π-calculus process has to execute to mimic a capability) and of aborting trace (representing the computation that a π-calculus process executes when the simulation of a capability cannot succeed). Thus, the encoding may introduce loops, but, as it will be shown, the number of steps of any trace, therefore of any aborting trace, is limited, and the number of states of the transition system of the encoding processes still remains finite. In particular, an aborting trace makes a sort of backtracking, leaving the involved sub-processes in the same starting configurations. We also discuss two run-time support methods to make these loops harmless at execution time. Our work defines a relatively simple, direct, and precise translation that reproduces the ambient structure by means of channel links, and keeps track of the dissolving of an ambient.

Information

Type
Paper
Copyright
Copyright © Cambridge University Press 2016