×

zbMATH — the first resource for mathematics

On bisimulations for the asynchronous \(\pi\)-calculus. (English) Zbl 0915.68009
Summary: The asynchronous \(\pi\)-calculus is a variant of the \(\pi\)-calculus where message emission is non-blocking. Honda and Tokoro have studied a semantics for this calculus based on bisimulation. Their bisimulation relies on a modified transition system where, at any moment, a process can perform any input action.
In this paper, we propose a new notion of bisimulation for the asynchronous \(\pi\)-calculus, defined on top of the standard labelled transition system. We give several characterizations of this equivalence including one in terms of Honda and Tokoro’s bisimulation, and one in terms of barbed equivalence. We show that this bisimulation is preserved by name substitutions, hence by input prefix. Finally, we give a complete axiomatization of the (strong) bisimulation for finite terms.

MSC:
68M10 Network design and communication in computer systems
Software:
Pict
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Agha, G., Actors: A model of concurrent computation in distributed systems, (1986), MIT-Press Cambridge, MA
[2] Berry, G.; Boudol, G., The chemical abstract machine, Theoret. comput. sci., 96, 217-248, (1992) · Zbl 0747.68013
[3] Boreale, M.; Sangiorgi, D., Some congruence properties for π-calculus bisimilarities, () · Zbl 0902.68117
[4] Boudol, G., Asynchrony and the π-calculus, () · Zbl 0944.68120
[5] Dam, M.; Dam, M., Model checking mobile processes, (), SICS report RR94:1, 22-36, (1994), Full version in
[6] Fournet, C.; Gonthier, G., The reflexive CHAM and the join-calculus, ()
[7] Hansen, M.; Kleist, J.; Hüttel, H., Bisimulations for asynchronous mobile processes, ()
[8] Honda, K.; Tokoro, M., An object calculus for asynchronous communication, ()
[9] Honda, K.; Tokoro, M., On asynchronous communication semantics, ()
[10] Honda, K.; Yoshida, N., On reduction based process semantics, Theoret. comput. sci., 151, 437-486, (1995) · Zbl 0871.68122
[11] Milner, R., Communication and concurrency, () · Zbl 0683.68008
[12] Milner, R., Functions as processes, Math. struct. comput. sci., 2, 2, 119-141, (1992) · Zbl 0773.03012
[13] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile process, Inform. and comput., 100, 1, 1-77, (1992), Parts 1-2
[14] Milner, R.; Sangiorgi, D., Barbed bisimulation, ()
[15] Nestmann, U.; Pierce, B., Decoding choice encodings, () · Zbl 1003.68080
[16] Pierce, B.; Turner, D., Pict: a programming language based on the π-calculus, Tech. report, indiana university, (1997), to appear.
[17] Sangiorgi, D., A theory of bisimulation for the π-calculus, () · Zbl 0835.68072
[18] Sangiorgi, D., Lazy functions and mobile processes, (), Invited for Festschrift Volume in Honor of Robin Milner’s 60th birthday, Cambridge Press, to appear. · Zbl 0956.68081
[19] Tel, G., Introduction to distributed algorithms, (1995), Cambridge University Press Cambridge
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.