The various π-calculi

Get Complete Project Material File(s) Now! »

The various π-calculi

Introduction

Several models for communication have been proposed in the literature. The kind of models known as Process Calculi consists of formalisms in which pro-cesses are specified syntactically by a grammar and semantically by a set of (structural) transition rules which define their operational behavior.
The first process calculi proposed in literature (CSP [BHR84, Hoa85], CCS [Mil80, Mil89], ACP [BK84]) were all based on synchronous communication primitives. This is because synchronous communication was considered some-what more basic, while asynchronous communication was considered a derived concept that could be expressed using buffers (see, for instance, [Hoa85]). Some early proposals of calculi based purely on asynchronous communication were based on forcing the interaction between processes to be always mediated by buffers [BKT84, dBKP92].
At the beginning of the 90’s, asynchronous communication became much more popular thanks to the diffusion of the Internet and the consequent increased in-terest for widely distributed systems. The elegant mechanism for asynchronous communication (the asynchronous send) proposed in the asynchronous π-calculus [HT91, Bou92] was very successful, probably because of its simple and basic nature, in line with the tradition of process calculi. Thus it rapidly became the standard approach to asynchronism in the community of process calculi, and it was adopted, for instance, also in Mobile Ambients [CG00]. A commu-nication primitive (tell ) similar to the asynchronous send was also proposed, independently, within the community of Concurrent Constraint Programming [SRP91a].
In the following, we present different variants of the π-calculus, including the synchronous and asynchronous π-calculus, as well as intermediate languages, which use synchronization primitives different from the ones of those two cal-culi.

The synchronous π-calculus: πs

The synchronous calculus is the most expressive calculus of the π-calculus fam-ily. It was originally introduced by Robin Milner, Joachim Parrow and David Walker. The model is an extension of the Calculus of Communicating Systems [Mil80, Mil89] (CCS), adding the possibility of transmitting a message between two processes trough a communication channel in order to allow dynamic re-configuration of the network and communication capabilities.
Indeed, in the π-calculus, messages and channels are the same objects, referred as names. It is then possible to send to a process a new channel name, allowing this process to communicate trough this channel. As for the λ-calculus, where everything is a function, in the π-calculus everything is a name.
Definition 1.1.1 Let N be a countable infinite set. We call the elements of N the names. If x is a name, then x is the co-name of x.
A process in the π-calculus is built using these names and the following syn-tax:
Definition 1.1.2 A π-calculus process is an element generated by the following grammar:
P, Q, . . . := 0 xz.P x(y).P P + Q νxP P | Q !P
The labels for the transitions in the πa-calculus are:
l, m, . . . := xy xy x(y) τ
The meaning of the grammar is as follow:
• The 0 process is a process that cannot do anything
• xz.P is a process that sends the name z on the channel x, then proceeds by the execution of the process P . It is refered as a sending prefix or sending continuation.
• x(y).P is a process that waits for the reception of a value on the channel x, and then follows with the execution of P , where all occurrences of y have been replaced by the received value. It is refered as a input prefix.
• P + Q is a process that that can proceed either as P or as Q. As soon as the transition from one process is executed, the other is dismissed.
• νxP is the process P where all occurrences of x are considered as locally bound. Any other occurrence of x which is not under the scope of this binder cannot interact with these local occurrences.
• P | Q is a parallel composition of the processes P and Q. The transitions of P | Q are those of either P or Q, or the result of any communication between them.
• !P is a process that can spawn an unbounded number of parallel copies of P .
The transition labels denotes the various actions that a process can do:
• xy stands for the reception of the value y over the channel x
• xy stands for the sending of the value y over the channel x
• x(y) stands for the sending of the private value y over the channel x. This action allows a process to communicate a private name to another process, creating a private link between them.
• τ stands for the silent (internal) action
If we consider the process x(y).P or νyP , the name y in both cases is a local name, bound to the scope of the process itself. If the name y appears in the context of another process, it has a different scope and cannot interact with the name y as referred by the first process. The set of such bound names of a process and the set of its free names are used to discriminate which names can be used to interact with other processes. They are defined as follows:
Definition 1.1.3 ([SW01], Definition 1.1.2 )
In each of νzP and x(z).P , the displayed occurence of z is binding with scope P . An occurence of a name in a process is bound if it is, or it lies into the scope of, a binding occurence of a name. An occurence of a name in a process is free if it is not bound. fn(P ) (resp. bn(P )) stands for the free names of P (resp. bound names of P ).
Bound names are names that are binded internaly. Hence, we can apply α-renaming on bounded names. More generally, we define a notion of renaming for the processes of the π-calculus.
Definition 1.1.4 ([SW01], Definition 1.1.5 )
Let P be a process of the π-calculus.
• If the name w does not occur in P , then P [w/z] is the process obtained by replacing each free occurence of z by w.
• A change of bound name is the replacement of a subterm x(z).Q of P by x(w).Q[w/z], or the replacement of a subterm νzP by νwQ[w/z], where in each case w does not occur in Q.
• Any process Q is an α-renaming of P if it can be obtained by a finite number of changes of bound name in P .
We want to enforce some symmetries and obvious equivalences between pro-cesses. Hence, we define an equivalence relation between processes, to reflect, for instance, the fact that we want: P | Q ≡ Q | P .
Definition 1.1.5 (structural congruence)
The relation ≡ is the smallest congruence over processes satisfying:
• α-conversion on bound names
• The commutative monoid laws for parallel and sum composition with 0 as identity
• νx(P | Q) ≡ P | νxQ when x fn(P )
• νx0 ≡ 0
• νxνxP ≡ νxP
• νxνyP ≡ νyνxP
• νxz(t).P ≡ z(t).νxP when z = x and t = x
The structural congruence is convenient in order to define the operational se-mantics of the language, as explained below. The structural congruence rep-resents the static equalities that we want to achieve between processes. This relation is used to match processes that are not syntactically equal, but for which the equality should be implicit, like when renaming bound names. Hence, it is very important that it is decidable since it is used often when computing the possible transitions of a process. In particular, the decidability of this relation is not known when adding the scope extrusion rules, such as νx(P | Q) ≡ P | νxQ when x fn(P ) and the rule !P ≡ P | !P . The decidability of the structural congruence when including replication is discussed in details in [EG99]. In par-ticular, it is proved that, when adding also other rules such as !!P ≡ !P or !(P | Q) ≡ !P | !Q, then the structural congruence is decidable. Since we do not need the structural replication rule, we avoid adding any of them in the relation.
The operational semantics of the π-calculus is defined in Table 1.1. It formalizes the meaning of the grammar, as explained above. It is a labeled transition system where labels are the transition labels given in Definition 1.1.
The rule (open) formalizes the sending of a private value. Hence, the ν binding is removed since the value has been sent outside of the scope of the process. However, when placed in parallel with another process, this value should not match another value. For instance if P = yt | νy(xy.y(v)), then we obviously x(y) do not want that: P → yt | y(v) since the name y in yt should not be the same. Hence, the (cong) rule is mandatory. Using it, we should state that: xz
P ≡ yt | νz(xz.z(v)) and then: P → yt | z(v). The (close) rule is entailed by the rules (sync), (ν) and (cong), hence it may not always be present in some further operational semantics.
The semantics written in this document is the early semantics, in contrast to the late semantics. In the late semantics, the input process P = x(y).Q only x(y) has a single transition P → Q and the name substitution is done in the com-munication rule, i.e. the rule for the parallel operator. The late semantics is more convenient for implementations of the language since the input process has only one single transition, while in the early semantics, there are infinitely
many of them. On the other hand, reasoning on the transitions generated by the late semantics can be more difficult, since one has to take into account the fact that the received value has not yet been substituted in the resulting process. Finally, the bisimilarities1 associated to those two semantics are different, the bisimulation associated to the late semantics being more restrictive than the one entailed by the early semantics. This issue is discussed in Section 3.1.
When clear from the context, we may use short-hand notations for some pro-cesses, namely: x(y) = x(y).0, xy = xy.0, x.P = x(v).P , where v f n(P ), x.P = xv.P where v f n(P ), and τ = νx(x | x).

The various asynchronous π-calculi.

The π-calculus models communications using a synchronous rule. Indeed, when two processes communicate with each other, the two operations, sending and receiving, are done in a single step. The transition is then atomic and hence synchronous:
xz.P | x(y).Q −τ→ P | Q[z/y]
As explained in the introduction, this does not apply quite easily to model most of the communications in real life, since for almost all of them, the sending and receiving operations do not happen at the same time. Furthermore, with the synchronous rule the sending process knows precisely when its message has 1 defined in Section 1.2
been received. In [Pal97], the author shows that there is an expressivity gap, depending on the possibility to communicate synchronously or not.
The πa-calculus was introduced, simultaneously in [Bou92] and [HT91]. The πa-calculus restricts the grammar of the π-calculus in order to remove operations that implies some sort of synchronism. The operational semantics remains the same with some small modifications, which are mainly restrictions that reflects the new restricted grammar.
Similarly, the possibility to execute input, output or mixed choices like (resp.) x(y).P + z(t).Q , xy + xy.Q or xy.P + z(t).Q can be argued to be a synchronous operation. Consequently, similarly restricted versions of the π-calculus have been proposed to reflect these considerations.
We will present here tree variants of these asynchronous languages, and prove simple properties about them. These properties will be usefull later to study the natural representation of the communications that each calculus model. Each of these properties are inherited from the less restrictive languages by the most restrictive ones.

The πsc -calculus

This is a fragment of the synchronous π-calculus where the general choice is replaced by separate choice: choices are prefixed by a set of actions of the same type, either sending actions or reception actions.
The restriction is motivated by the fact that the possibility, for a process, to choose wether it will receive a new value or send a message is not easy to implement. This is for instance studied in [PH05b]. Intuitively, this relates to the possibility to communicate in full-duplex. As argued in the introduction, this possibility is not always granted, and it is even hardly the case. Hence, this language restricts the communication primitives so as to remove this possibility in the core language.
Here I is a set of indexes. Note that we have omitted the process 0 since it can be represented as the empty summation.
The definition of the transition semantics is the same as the one of the π-calculus (Table 1.1).
The crucial property here is a confluence that holds in the separate-choice π-calculus, as proved in [Pal03](Lemma 4.1). This property, which is present in many asynchronous communication models, is the central result for proving the separation between the synchronous π-calculus and the asynchronous one. Indeed, the results is obtained by proving that the application of this confluence gives the possibility to find incorrect asynchronous executions for the problem of distributed symmetric consensus.

Table of contents :

I Asynchronous communications 
1 Concurrent communication models. 
1.1 The various π-calculi
1.2 Bisimulations and asynchronous communications
2 Communicating trough buffers 
2.1 Buffers, stacks, queues and bags
2.2 The πB-calculus
2.3 Encodings from and to the πa-calculus and πB-calculus
2.4 Impossibility result for the other types of buffer
II Asynchronous behavior 
3 Equivalent behavior in the π-calculus 
3.1 The late semantics
3.2 Bisimilarities and congruences
3.3 The asynchronous case
4 Causality and asynchrony: speeding up the scheduler 
4.1 Bunched Labeled Transition Systems
4.2 Bunched transition system for the πa-calculus
4.3 Further discussions
III Asynchronous probabilistic executions 
5 Probabilistic Concurrent Constraint Programming. 
5.1 The Constraint System
5.2 The language
5.3 Application: Crowds anonymous routing
6 Denotational semantics for the CCP+P 
6.1 Valuations
6.2 Vector cones of simple valuations
6.3 Denotational semantics
IV Application: the dinning cryptographers reloaded 
7 Anonymous protocols: the dining cryptographer 
7.1 The nondeterministic approach to anonymity
7.2 The dining cryptographers’ problem
8 Toward an automated probabilistic anonymity checker 
8.1 Probabilistic automata
8.2 Our framework for probabilistic anonymity
8.3 The various notions of anonymity
8.4 Toward an automatic probabilistic checker

GET THE COMPLETE PROJECT