zbMATH — the first resource for mathematics

A hierarchy of equivalences for asynchronous calculi. (English) Zbl 1066.68088
Summary: We generate a natural hierarchy of equivalences for asynchronous name-passing process calculi from simple variations on Milner and Sangiorgi’s definition of weak barbed bisimulation. The \(\pi\)-calculus, used here, and the join calculus are examples of such calculi. We prove that barbed congruence coincides with Honda and Yoshida’s reduction equivalence, and with asynchronous labeled bisimulation when the calculus includes name matching, thus closing those two conjectures. We also show that barbed congruence is coarser when only one barb is tested. For the \(\pi\)-calculus, it becomes a limit bisimulation, whereas for the join calculus, it coincides with both fair testing equivalence and with the weak barbed version of Sjödin and Parrow’s coupled simulation.

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI
[1] Abadi, M.; Fournet, C., Mobile values, new names, and secure communication, (), 104-115 · Zbl 1323.68398
[2] Abadi, M.; Fournet, C.; Gonthier, G., Authentication primitives and their compilation, (), 302-315 · Zbl 1323.68178
[3] Abadi, M.; Fournet, C.; Gonthier, G., Secure implementation of channel abstractions, Information and computation, 174, 1, 37-83, (2002) · Zbl 1009.68084
[4] Abadi, M.; Gordon, A.D., Reasoning about cryptographic protocols in the spi calculus, (), 59-73
[5] Agha, G.; Mason, I.; Smith, S.; Talcott, C.L., A foundation for actor computation, Journal of functional programming, 7, 1, 1-72, (1997) · Zbl 0870.68091
[6] Amadio, R.M.; Castellani, I.; Sangiorgi, D., On bisimulations for the asynchronous π-calculus, Theoretical computer science, 195, 2, 291-324, (1998) · Zbl 0915.68009
[7] Boreale, M.; De Nicola, R., Testing equivalence for mobile processes, Information and computation, 120, 2, 279-303, (1995) · Zbl 0835.68073
[8] G. Boudol, Asynchrony and the π-calculus (note), Rapport de Recherche 1702, INRIA Sophia-Antipolis, May 1992
[9] Brinksma, E.; Rensink, A.; Vogler, W., Fair testing, (), 313-327
[10] Brinksma, E.; Rensink, A.; Vogler, W., Applications of fair testing, ()
[11] De Nicola, R.; Hennessy, M.C.B., Testing equivalences for processes, Theoretical computer science, 34, 83-133, (1984) · Zbl 0985.68518
[12] Fournet, C.; Gonthier, G., The join calculus: a language for distributed mobile programming, (), 268-332 · Zbl 1065.68071
[13] C. Fournet, The join-calculus: a calculus for distributed mobile programming, Ph.D. thesis, Ecole Polytechnique, Palaiseau, November 1998 · Zbl 1065.68071
[14] Fournet, C.; Gonthier, G., The reflexive chemical abstract machine and the join-calculus, (), 372-385
[15] Fournet, C.; Gonthier, G., A hierarchy of equivalences for asynchronous calculi (extended abstract), (), 844-855 · Zbl 0909.03030
[16] Fournet, C.; Laneve, C., Bisimulations in the join-calculus, Theoretical computer science, 266, 1-2, 569-603, (2001) · Zbl 0989.68098
[17] Fournet, C.; Laneve, C.; Maranget, L.; Rémy, D., Implicit typing à la ML for the join-calculus, (), 196-212
[18] Fournet, C.; Lévy, J.-J.; Schmitt, A., An asynchronous, distributed implementation of mobile ambients, () · Zbl 0998.68537
[19] van Glabbeek, R.J., The linear time – branching time spectrum II; the semantics of sequential systems with silent moves (extended abstract), (), 66-81
[20] Hennessy, M., Algebraic theory of processes, (1988), The MIT Press · Zbl 0744.68047
[21] Honda, K.; Tokoro, M., On asynchronous communication semantics, (), 21-51
[22] Honda, K.; Yoshida, N., On reduction-based process semantics, Theoretical computer science, 152, 2, 437-486, (1995) · Zbl 0871.68122
[23] C. Laneve, May and must testing in the join-calculus, Technical Report UBLCS 96-04, University of Bologna, March 1996, Revised: May 1996
[24] Merro, M.; Sangiorgi, D., On asynchrony in name-passing calculi, (), 856-867 · Zbl 0910.03019
[25] Milner, R., A calculus of communicating systems, Lecture notes in computer science, vol. 92, (1980), Springer-Verlag · Zbl 0452.68027
[26] Milner, R., Communication and concurrency, (1989), Prentice Hall New York · Zbl 0683.68008
[27] Milner, R., The polyadic π-calculus: a tutorial, ()
[28] Milner, R., Communication and mobile systems: the π-calculus, (1999), Cambridge University Press Cambridge · Zbl 0942.68002
[29] Milner, R.; Sangiorgi, D., Barbed bisimulation, (), 685-695
[30] J.H. Morris Jr. Lambda-calculus models of programming languages, Ph.D. dissertation, MIT, December 1968, Report No. MAC-TR-57
[31] Natarajan, V.; Cleaveland, R., Divergence and fair testing, () · Zbl 1412.68155
[32] Nestmann, U.; Pierce, B.C., Decoding choice encodings, Information and computation, 163, November, 1-59, (2000) · Zbl 1003.68080
[33] Park, D.M.R., Concurrency and automata on infinite sequences, Lecture notes in computer science, vol. 104, (1980), Springer-Verlag
[34] Parrow, J.; Sjödin, P., Multiway synchronization verified with coupled simulation, (), 518-533
[35] Parrow, J.; Sjödin, P., The complete axiomatization of cs-congruence, (), 557-568 · Zbl 0941.68573
[36] D. Sangiorgi, Expressing mobility in process algebras: first-order and higher-order paradigms, Ph.D. thesis, Department of Computer Science, University of Edinburgh, 1992
[37] Sangiorgi, D., A theory of bisimulation for the π-calculus, Acta informatica, 33, 69-97, (1996) · Zbl 0835.68072
[38] Sangiorgi, D., On the bisimulation proof method, Journal of mathematical structures in computer science, 8, 447-479, (1998) · Zbl 0916.68057
[39] Sangiorgi, D.; Milner, R., The problem of “weak bisimulation up to”, (), 32-46
[40] Sangiorgi, D.; Walker, D., The pi-calculus: a theory of mobile processes, (2001), Cambridge University Press · Zbl 0981.68116
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.