zbMATH — the first resource for mathematics

What is a “good” encoding of guarded choice? (English) Zbl 1046.68625
Summary: The \(\pi\)-calculus with synchronous output and mixed-guarded choices is strictly more expressive than the \(\pi\)-calculus with asynchronous output and no choice. This result was recently proved by C. Palamidessi and, as a corollary, she showed that there is no fully compositional encoding from the former into the latter that preserves divergence-freedom and symmetries. This paper argues that there are nevertheless “good” encodings between these calculi. In detail, we present a series of encodings for languages with (1) input-guarded choice, (2) both input- and output-guarded choice, and (3) mixed-guarded choice, and investigate them with respect to compositionality and divergence-freedom. The first and second encoding satisfy all of the above criteria, but various “good” candidates for the third encoding – inspired by an existing distributed implementation – invalidate one or the other criterion. While essentially confirming Palamidessi’s result, our study suggests that the combination of strong compositionality and divergence-freedom is too strong for more practical purposes.

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Amadio, R.M.; Castellani, I.; Sangiorgi, D., On bisimulations for the asynchronous π-calculus, Theoret. comput. sci., 195, 291-324, (1998) · Zbl 0915.68009
[2] Arun-Kumar, S.; Hennessy, M., An efficiency preorder for processes, Acta inform., 29, 737-760, (1992) · Zbl 0790.68039
[3] Amadio, R.M., An asynchronous model of locality, failure, and process mobility, () · Zbl 0954.68072
[4] Ben-Or, M., Another advantage of free choice: completely asynchronous agreement protocols (extended abstract), Proceedings of PODC ’83, (1983), ACM New York, p. 27-30
[5] Bernstein, A., Output guards and nondeterminism in “communicating sequential processes”, ACM trans. programming lang. systems, 2, 234-238, (1980)
[6] Busi, N.; Gorrieri, R.; Zavattaro, G., On the Turing-equivalence of linda coordination primitives, () · Zbl 0911.68139
[7] Bougé, L., On the existence of symmetric algorithms to find leaders in networks of communicating sequential processes, Acta inform., 25, 179-201, (1988) · Zbl 0621.68011
[8] Boudol, G., Asynchrony and the π-calculus, Rapport de recherche, (1992)
[9] Buckley, G.; Silberschatz, A., An effective implementation for the generalized input – output construct of CSP, ACM trans. programming lang. systems, 5, 223-235, (1983) · Zbl 0516.68026
[10] Bellin, G.; Scott, P., On the π-calculus and linear logic, Theoret. comput. sci., 135, 11-65, (1994) · Zbl 0817.03001
[11] Fournet, C.; Gonthier, G., The reflexive chemical abstract machine and the join-calculus, Proceedings of POPL ’96, (1996), ACM New York, p. 372-385
[12] Fournet, C.; Gonthier, G., A hierarchy of equivalences for asynchronous calculi, (), 844-855 · Zbl 0909.03030
[13] Honda, K. 1992, Notes on soundness of a mapping from π-calculus to ν-calculus. [Comments added in October 1993]
[14] Honda, K.; Tokoro, M., On asynchronous communication semantics, (), 21-51
[15] Knabe, F., A distributed protocol for channel-based communication with choice, Comput. artif. intell., 12, 475-490, (1993)
[16] Kobayashi, N., A partially deadlock-free typed process calculus, Proceedings of LICS ’97, (1997), Comput. Soc. Press New York, p. 128-139
[17] Kumar, D.; Silberschatz, A., A counter-example to an algorithm for the generalized input-output construct of CSP, Inform. process. lett., 61, 287, (1997) · Zbl 0925.68085
[18] Lamport, L., A new solution of Dijkstra’s concurrent programming problem, J. assoc. comput. Mach., 17, 453-455, (1974) · Zbl 0281.68004
[19] Leth, L.; Thomsen, B., Some facile chemistry, Formal aspects comput., 7, 314-328, (1995)
[20] Milner, R., The polyadic π-calculus: A tutorial, ()
[21] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, I/II, Inform. and comput., 100, 1-77, (1992) · Zbl 0752.68037
[22] Milner, R.; Sangiorgi, D., Barbed bisimulation, (), 685-695
[23] Nestmann, U., On determinacy and nondeterminacy in concurrent programming, (1996), Universität ErlangenTechnische Fakultät
[24] Nestmann, U.; Pierce, B.C., Decoding choice encodings, (), 179-194 · Zbl 1003.68080
[25] Palamidessi, C., Comparing the expressive power of the synchronous and the asynchronous π-calculus, Proceedings of POPL ’97, (1997), ACM New York, p. 256-265
[26] Parrow, J.; Sjödin, P., Multiway synchronization verified with coupled simulation, (), 518-533
[27] Pierce, B.C.; Sangiorgi, D., Typing and subtyping for mobile processes, Math. struct. comput. sci., 6, 409-454, (1996) · Zbl 0861.68030
[28] Reppy, J., CML: A higher-order concurrent language, Proceedings of PLDI ’91, (1991), ACM New York, p. 293-259
[29] Rabin, M.O.; Lehmann, D., On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problems, (), 333-352
[30] Sangiorgi, D., Expressing mobility in process algebras: first-order and higher-order paradigms, (1993), University of EdinburghLFCS
[31] Sangiorgi, D., The name discipline of uniform receptiveness, (), 303-313 · Zbl 0930.68035
[32] Thomsen, B.; Leth, L.; Kuo, T.-M., A facile tutorial, (), 278-298
[33] Victor, B.; Parrow, J., Constraints as processes, (), 389-405
[34] Yoshida, N., Graph types for monadic mobile processes, (), 371-386
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.