A calculus of mobile processes. I.

*(English)*Zbl 0752.68036Summary: We present the \(\pi\)-calculus, a calculus of communicating systems in which one can naturally express processes which have changing structure. Not only may the component agents of a system be arbitrarily linked, but a communication between neighbours may carry information which changes that linkage. The calculus is an extension of the process algebra CCS, following work by H. Engberg and M. Nielsen [A calculus of communicating systems with label-passing, Report DAIMI PB–208, Computer Science Department, University of Aarhus (1986)] who added mobility to CCS while preserving its algebraic properties. The \(\pi\)-calculus gains simplicity by removing all distinction between variables and constants; communication links are identified by names, and computation is represented purely as the communication of names across links. After an illustrated description of how the \(\pi\)-calculus generalises conventional process algebras in treating mobility, several examples exploiting mobility are given in some detail. The important examples are the encoding into the \(\pi\)-calculus of higher-order functions (the \(\lambda\)-calculus and combinatory algebra), the transmission of processes as values, and the representation of data structures as processes. The paper continues by presenting the algebraic theory of strong bisimilarity and strong equivalence, including a new notion of equivalence indexed by distinctions — i.e., assumptions of inequality among names. These theories are based upon a semantics in terms of a labeled transition system and a notion of strong bisimulation, both of which are expounded in detail in a companion paper. We also report briefly on work-in-progress based upon the corresponding notion of weak bisimulation, in which internal actions cannot be observed.

##### MSC:

68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

##### Keywords:

calculus of communicating systems; processes; process algebra; mobility; strong bisimilarity; strong equivalence; distinctions; labeled transition system
PDF
BibTeX
XML
Cite

\textit{R. Milner} et al., Inf. Comput. 100, No. 1, 1--40 (1992; Zbl 0752.68036)

Full Text:
DOI

##### References:

[1] | Abramsky, S., The lazy lambda calculus, () · Zbl 0779.03003 |

[2] | Astesiano, E.; Zucca, E., Parametric channels via label expressions in CCS, Theoret. comput. sci., 33, 45-64, (1984) · Zbl 0542.68017 |

[3] | Bergstra, J.A.; Klop, J.-W., Algebra of communicating processes with abstraction, Theoret. comput. sci., 33, 77-121, (1985) · Zbl 0579.68016 |

[4] | \scBoudol, G. (1988), private communication. |

[5] | Clinger, W.D., (), AI-TR-633 |

[6] | Engberg, U.; Nielsen, M., (), Report DAIMI PB-208 |

[7] | Hoare, C.A.R., () |

[8] | Leinwand, S.; Goguen, J.A.; Winkler, T., Cell and ensemble architecture for the rewrite rule machine, (), 869-878 |

[9] | Milner, R., () |

[10] | Milner, R., Functions as processes, J. math. stud. comput. sci., (1990), to appear · Zbl 0766.68036 |

[11] | Milner, R.; Parrow, J.G.; Walker, D.J.; Milner, R.; Parrow, J.G.; Walker, D.J., (), Information and computation, 100, 41-77, (1992), and |

[12] | Nielsen, F., The typed λ-calculus with first-class processes, (), Lecture Notes in Computer Science |

[13] | Ong, C.-H.L., Fully abstract models of the lazy lambda calculus, (), 368-376 |

[14] | Reisig, W., Petri nets, () · Zbl 0521.68057 |

[15] | Sleep, M.R.; Kennaway, J.R., The zero assignment parallel processor (ZAPP) project, (), 250-269 |

[16] | Thomsen, B., A calculus of higher-order communicating systems, () · Zbl 0974.68109 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.