A well-behaved LTS for the Pi-calculus Abstract 2007

Abstract:  The pi-calculus and its many variations have received much attention in the literature. We discuss the standard early labelled transition system (lts) and outline an approach which decomposes the system into two components, one of which is presented in detail. The advantages of using the decomposition include a more complete understanding of the treatment of bound outputs in Pi as well as an lts which is more robust with respect to the addition and removal of language features. The present paper serves as an overview of some of the techniques involved and some of the goals of the ongoing work. Keywords: Pi-calculus, process calculi, semantics, labelled transition systems The Pi-calculus [2, 10] and its many variants have been widely studied in the literature. A valid criticism is that in many cases the theory is heavily optimised for the particular variant studied ? meaning that while often a pleasant simplicity is achieved in the presentation of basic theoretical results, the resulting formalism is heavily locally optimised and often not robust with respect to the equivalences or language features considered. In this paper we outline an approach which promises to give a more robust method of providing a labelled transition system on which, for instance, bisimilarity agrees with contextual equivalence. The technique is also more amenable to generalisation, in the pursuit of capturing a wider family of calculi. The Pi-calculus, roughly, extends the binary synchronisations along a channel/name, familiar from ccs, with the ability to pass names as arguments. Thus, the input prefix becomes a binder and the synchronisation itself results in a substitution of the communicated name for the bound variable. The calculus inherits another binder from ccs ? the restriction operator. The ability to pass names as part of a synchronous communication means that it behaves rather differently in this setting- in particular, the scope of a restriction, static in ccs, becomes dynamic essentially because restricted names can be communicated along public channels. Additionally, it behaves somewhat like a global generator of new-names- since a-conversion ensures that whichever concrete name is chosen