A multiset semantics for the pi-calculus with replication

Reviewer: D. John Cooke

The small pi-calculus (a recognized subset of the pi-calculus that does not have a choice operator and that includes countable replication rather than recursion) is addressed. The semantic model is a place/transition net, the (multiset) transitions of which are obtained by compositional mapping from processes in the small pi-calculus. Using a name-generation system to handle the nesting of the restriction construction, the author gives a net-based description of “programs” expressed in the calculus. This is illustrated by a good example. The relationship between the language in the paper and the pi-calculus (and the small pi-calculus) must be carefully noted. The new system is strictly a variant of the small pi-calculus in that it satisfies extra laws pertaining to structural congruence as applied to the repetition construct. These do not hold in the “proper” small pi-calculus, and neither does one of the restriction laws. The author suggests that these rules should hold (and hence he has arguably produced a language that has a more natural semantics). His language cannot, however, cope with the choice operator of the full pi-calculus. Notwithstanding these observations by the author, the work contributes to a better understanding of the derivatives of calculus of communicating systems (CCS). All necessary proofs are included in an eight-page section of the paper and are easy to follow. This paper is a reworking of an earlier conference presentation and is succeeded by a Leiden technical report , in which extra details and developments are given.