×

Some congruence properties for \(\pi\)-calculus bisimilarities. (English) Zbl 0902.68117

Summary: Both for interleaving and for non-interleaving semantics, several variants of a \(\pi\)-calculus bisimilarity can be given which differ on the requirements imposed on name instantiations. Examples are the late, early, open and ground variants. The ground variant is the simplest because it places no requirements on name instantiations. With the exception of open bisimilarities, none of the bisimilarity considered in the literature is a congruence relation on the full \(\pi\)-calculus language. We show that in the case of (certain forms of) causal bisimulation the late, early, open and ground variants coincide and are congruence relations in the sublanguage of the \(\pi\)-calculus without matching. We also show that to obtain the same results in the case of the interleaving bisimilarity, in addition to forbidding matching it is necessary to constrain the output prefix.

MSC:

68Q55 Semantics in the theory of computing
Full Text: DOI

References:

[1] Boreale, M.; Sangiorgi, D., A fully abstract semantics for causality in the π-calculus, (Technical Report ECS-LFCS-94-297 (1994), LFCS, Dept. of Comp. Sci., Edinburgh Univ), to appear in Acta Inform. · Zbl 0908.68103
[2] An extract appeared in Proc. STACS’95, Lecture Notes in Computer Science, vol. 900, Springer, Berlin.; An extract appeared in Proc. STACS’95, Lecture Notes in Computer Science, vol. 900, Springer, Berlin.
[3] de Bruijn, N. G., Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem, Indag. Math., 34, 5, 381-392 (1972) · Zbl 0253.68007
[4] Degano, P.; Darondeau, P., Causal trees, (15th ICALP. 15th ICALP, Lecture Notes in Computer Science, vol. 372 (1989), Springer: Springer Berlin), 234-248
[5] Hansen, M.; Hüttel, H.; Kleist, J., Bisimulations for asynchronous mobile processes, (Proc. Tbilisi Symp. on Language, Logic, and Computation, 1996. Proc. Tbilisi Symp. on Language, Logic, and Computation, 1996, BRICS Report No. EP-95-HHK (1996), Aalborg University: Aalborg University Denmark), also available as
[6] Honda, K., Two bisimilarities for the ν-calculus, (Tech. Report 92-002 (1992), Keio University)
[7] Honda, K.; Tokoro, M., On asynchronous communication semantics, (Tokoro, M.; Nierstrasz, O.; Wegner, P.; Yonezawa, A., ECOOP’91 Workshop on Object Based Concurrent Programming. ECOOP’91 Workshop on Object Based Concurrent Programming, Geneva, Switzerland, 1991. ECOOP’91 Workshop on Object Based Concurrent Programming. ECOOP’91 Workshop on Object Based Concurrent Programming, Geneva, Switzerland, 1991, Lecture Notes in Computer Science, vol. 612 (1992), Springer: Springer Bertin), 21-51
[8] Kiehn, A., Revision of Local and Global Causes, Report TUM-I9132 (1991) · Zbl 0834.68070
[9] (Bauer, F. L.; Brauer, W.; Schwichtenberg, H., Logic and Algebra of Specification (1993), LFCS, Dept. of Comp. Sci., Edinburgh Univ: LFCS, Dept. of Comp. Sci., Edinburgh Univ Berlin), Also in · Zbl 0818.68109
[10] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, Inform. Comput., 100, 1-77 (1992), (Parts I and II) · Zbl 0752.68037
[11] Pierce, B. C.; Rémy, D.; Turner, D. N., A typed higher-order programming language based on the picalculus, (Workshop on Type Theory and its Application to Computer Systems, Kyoto University (1993)) · Zbl 0939.68569
[12] Priami, C., Enhanced operational semantics for concurrency, (Ph.D. Thesis (1995), Department of Computer Science, Università di Pisa)
[13] Sangiorgi, D., On the bisimulation proof method, (Technical Report ECS-LFCS-94-299 (1994), LFCS, Dept. of Comp. Sci., Edinburgh Univ) · Zbl 0916.68057
[14] Sangiorgi, D., Lazy functions and mobile processes, (Technical Report RR-2515 (1995), INRIA: INRIA Sophia Antipolis), Festschrift volume in honor of Robin Milner’s 60th birthday, to appear, Cambridge Press, Cambridge. · Zbl 0956.68081
[15] Sangiorgi, D., A theory of bisimulation for the π-calculus, Acta Informatica, 33, 69-97 (1996) · Zbl 0835.68072
[16] Extended Abstract in Proc. CONCUR’93, Lecture Notes in Computer Science, vol. 715, Springer, Berlin.; Extended Abstract in Proc. CONCUR’93, Lecture Notes in Computer Science, vol. 715, Springer, Berlin.
[17] Sangiorgi, D., Theoret. Comput. Sci., 167, 2, 235-274 (1996), Full version in · Zbl 0874.68103
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.