π-Calculus

Abstract

In this chapter we outline the basic theory of a calculus of processes, called the π-calculus. It is not an exaggeration to affirm that the π-calculus plays for reactive systems the same foundational role that the λ-calculus plays for sequential systems. The key idea is to extend CCS with the ability to send channel names, i.e., π-calculus processes can communicate communication means. The term coined to refer to this feature is name mobility. The operational semantics of the π-calculus is only a bit more involved than that of CCS, while the abstract semantics is considerably more ingenious, because it requires a careful handling of names appearing in the transition labels. In particular, we show that two variants of strong bisimilarity arise naturally, called early and late, with the former coarser than the latter. We conclude by discussing weak variants of early and late bisimilarities together with compositionality issues.

What’s in a name? That which we call a rose by any other name would smell as sweet. (William Shakespeare)