The \pi-calculus

The \pi-calculus is a process calculus introduced by Robin Milner, Joachim Parrow, and David Walker in 1992.

Unlike older process calculi, such as CSP or CCS, the \pi-calculus puts the emphasis on mobility of processes. The main technical device by which that is achieved is that of names, and the notions of name generation and scope extrusion.

Syntax

There are many variations of the basic syntax of \pi-calculus. Here we will work with

P \Coloneqq \bar{x}y. P \mid x(y). P \mid \nu x. P \mid 0 \mid P + P \mid P\mathop{\mid}P \mid \text{!}P

There are many variants of this basic syntax. One may:

Replace the replication \text{!}P by a recursive process \textsf{rec } x. P, or a system of recursively defined equations (as in the original paper Milner et al. 1992).
Restrict the replication \text{!}P to a guarded replication \text{1} \alpha. P, where \alpha is a prefix. It is generally believed that guarded replications enjoy simpler algebraic laws, and thus many attempts at fully abstract model only guarded replications Fiore et al. 1996, 2002.
Add a match operator [x = y]P, and even a mismatch operator [x \neq y]P.
Make the sum P + Q guarded, i.e. require that both P and Q start with input/output prefixes.
make the sum indexed, i.e. \Sigma_{i \in I} P_i

Asynchronous pi-calculus

The asynchronous \pi-calculus arises by replacing the output prefix \bar{x}y. with a single process

\bar{x}y

which outputs y along x, and then stops. Thus, an output action may happen immediately (e.g. by putting the message y into a buffer that will be next read when an input on x is requested. By the structural congruence, this process \bar{x}y can 'float around' to reach its destination.

The asynchronous version of the \pi-calculus was introduced in Boudol 1992.

References

The \pi-calculus was introduced in

Milner, Robin, Joachim Parrow, and David Walker. 1992. ‘A Calculus of Mobile Processes, I’. Information and Computation 100 (1): 1–40. https://doi.org/10.1016/0890-5401(92)90008-4.

@article{milner_calculus_1992,
	title = {A calculus of mobile processes, {I}},
	volume = {100},
	issn = {08905401},
	doi = {10.1016/0890-5401(92)90008-4},
	number = {1},
	urldate = {2020-09-26},
	journal = {Information and Computation},
	author = {Milner, Robin and Parrow, Joachim and Walker, David},
	month = sep,
	year = {1992},
	pages = {1--40}

Some technical improvement to the original presentation, including structural congruence, appeared in

Milner, Robin. 1992. ‘Functions as Processes’. Mathematical Structures in Computer Science 2 (2): 119–141. https://doi.org/10.1017/S0960129500001407.

@article{milner_functions_1992,
	title = {Functions as processes},
	volume = {2},
	doi = {10.1017/S0960129500001407},
	number = {2},
	journal = {Mathematical Structures in Computer Science},
	author = {Milner, Robin},
	year = {1992},
	pages = {119--141}
}

A modern textbook account can be found in

Milner, Robin. 1999. Communicating and Mobile Systems: The π-Calculus. New York, NY, USA: Cambridge University Press.

@book{milner_communicating_1999,
	address = {New York, NY, USA},
	title = {Communicating and {Mobile} {Systems}: {The} π-calculus},
	isbn = {0-521-65869-1},
	publisher = {Cambridge University Press},
	author = {Milner, Robin},
	year = {1999}
}

The asynchronous \pi-calculus was introduced in

Boudol, Gérard. “Asynchrony and the Pi-Calculus.” Research Report. INRIA, 1992. https://inria.hal.science/inria-00076939.

@report{boudol_1992,
	title = {Asynchrony and the Pi-calculus},
	url = {https://inria.hal.science/inria-00076939},
	pages = {15},
	number = {{RR}-1702},
	institution = {{INRIA}},
	type = {Research Report},
	author = {Boudol, Gérard},
	date = {1992},
}

Fully abstract models for the \pi-calculus were given in the following papers, which both appeared at LICS 1996.

Stark, I. “A Fully Abstract Domain Model for the π-Calculus.” In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 36–42. IEEE, 1996. https://doi.org/10.1109/LICS.1996.561301.

@inproceedings{stark_1996,
	title = {A fully abstract domain model for the π-calculus},
	doi = {10.1109/LICS.1996.561301},
	pages = {36--42},
	booktitle = {Proceedings 11th Annual {IEEE} Symposium on Logic in Computer Science},
	publisher = {{IEEE}},
	author = {Stark, I.},
	date = {1996},
	file = {Stark - 1996 - A fully abstract domain model for the π-calculus.pdf:C\:\\Users\\tz20861\\Zotero\\storage\\DYPGZ9RB\\Stark - 1996 - A fully abstract domain model for the π-calculus.pdf:application/pdf},
}

Fiore, M.P., E. Moggi, and D. Sangiorgi. “A Fully-Abstract Model for the π-Calculus.” In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 43–54, 1996. https://doi.org/10.1109/LICS.1996.561302.

@inproceedings{fiore_1996,
	title = {A fully-abstract model for the $\pi$-calculus},
	doi = {10.1109/LICS.1996.561302},
	pages = {43--54},
	booktitle = {Proceedings 11th Annual {IEEE} Symposium on Logic in Computer Science},
	author = {Fiore, M.P. and Moggi, E. and Sangiorgi, D.},
	date = {1996},
}

Fiore, M.P., E. Moggi, and D. Sangiorgi. “A Fully Abstract Model for the π-Calculus.” Information and Computation 179, no. 1 (2002): 76–117. https://doi.org/10.1006/inco.2002.2968.

@article{fiore_2002,
	title = {A Fully Abstract Model for the $\pi$-calculus},
	volume = {179},
	doi = {10.1006/inco.2002.2968},
	pages = {76--117},
	number = {1},
	journaltitle = {Information and Computation},
	author = {Fiore, M.P. and Moggi, E. and Sangiorgi, D.},
	date = {2002},
}