Bisimulations for asynchronous mobile processes

Martin Hansen  Hans Hüttel^{∗}  Josva Kleist

BRICS^{†}, Department of Math. & Comp. Science Aalborg University Fredrik Bajersvej 7E 9220 Aalborg Ø Denmark

An important question in the theory of process calculi is when two processes can be said to exhibit the same behaviour and a number of behavioural equivalences have been proposed. Traditionally, the emphasis has been on studying the equivalences for ‘pure’ processes where communication does not involve the passing of data values. However, within the past few years there has been renewed interest in the study of value-passing as a consequence of the emergence of the π-calculus. Here Milner et. al. [6] have determined two variants of the notion of bisimulation, late and early bisimilarity, differing in the assumption of when a data value is instantiated. Most recently Sangiorgi [7] has proposed a new notion of bisimulation equivalence which he calls open bisimilarity. Sangiorgi formulates a sound and complete equational theory for open bisimilarity on finite (i.e. non-recursive) π-calculus terms.

An important theorem is that the three notions of bisimilarity are distinct within the π-calculus, with open bisimulation being strictly finer than late bisimulation which in turn is strictly finer than early bisimulation. The late/early distinction has been studied for the much coarser testing equivalence of Hennessy and De Nicola and it has been shown by Ingólfsdótir [5] and Boreale and De Nicola [1] that the late and early testing equivalences coincide, both for a process calculus with simple data values and conditional expression and for the π-calculus.

In this paper we consider Plain LAL, a mobile process calculus which differs from the π-calculus in the sense that the communication of data values happens asynchronously. Previously, Honda and Tokoro [4] and Boudol [2] have described so-called asynchronous π-calculi. However, they have not studied the notion of equivalence within this setting. The surprising result is that in the presence of asynchrony, the open, late and early bisimulation equivalences coincide. As the equivalences are one and the same, this leads us to formulate an equational theory which is sound for finite terms of Plain LAL.

∗E-mail: hans@iesd.auc.dk

†Basic Research in Computer Science, Centre of the Danish National Research Foundation

References

[1] Michele Boreale and Rocco De Nicola. Testing equivalences for mobile processes. In W.R. Cleaveland, editor, CONCUR ’92, number 630 in Springer LNCS, pages 2–16. Springer-Verlag, 1992.

[2] Gérad Boudol. Asynchrony and the π-calculus. Technical report, INRIA Sophia-Antipolis, 1992.

[3] Martin Hansen and Josva Kleist. Process calculi with asynchronous communication. Master’s thesis, Aalborg University, 1994.

[4] K. Honda and M. Tokoro. An object calculus for asynchronous communication. In ECOOP 91, volume 512 of Lecture Notes in Computer Science, pages 133–147. Springer-Verlag, 1991.

[5] Anna Ingólfsdóttir. Late and early semantics coincide for testing. Theoretical Computer Science, 1994. To appear.

[6] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes — part i and ii. Technical Report ECS-LFCS-89-85 and -86, Department of Computer Science, University of Edinburgh, 1989. Also published in Information and Computation, 100:1-77,1992.

[7] Davide Sangiorgi. A theory of bisimulation for the π-calculus. In E. Best, editor, Proceedings of CONCUR 93, volume 715 of Lecture Notes in Computer Science, pages 127–142. Springer-Verlag, 1993.