Symmetric electoral systems for ambient calculi

This paper compares the expressiveness of different fragments of ambient calculi via leader election problems. We consider Mobile Ambients (MA), Safe Ambients (SA) and the Push and Pull Ambient Calculus (PAC). Cardelli and Gordon encoded the asynchronous π-calculus into MA. Zimmer has shown that the synchronous π-calculus without choice can be encoded in pure (no communication) SA. We show that pure MA without restriction has symmetric electoral systems, that is, it is possible to solve the problem of electing a leader in a symmetric network. By the work of Palamidessi, this implies that this fragment of MA is not encodable (under certain conditions) in the π-calculus with separate choice. Moreover, we use the same technique to show that fragments of SA and PAC are not encodable (under certain conditions) in the π-calculus with separate choice. We also show that particular fragments of ambient calculi do not admit a solution to leader election problems, in the same way as the π-calculus with separate choice. This yields a fine-grained hierarchy within ambient calculi.