×

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.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[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, (Garlan, D.; Le Metayer, D., Proceedings of COORDINATION ’97. Proceedings of COORDINATION ’97, LNCS, 1282 (1997), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0954.68072
[4] Ben-Or, M., Another advantage of free choice: Completely asynchronous agreement protocols (Extended abstract), Proceedings of PODC ’83 (1983), ACM: 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, (Palamidessi, C.; Parrow, J., Proceedings of EXPRESS ’97. Proceedings of EXPRESS ’97, ENTCS, 7 (1997), Elsevier Science: Elsevier Science Amsterdam) · 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: ACM New York, p. 372-385
[12] Fournet, C.; Gonthier, G., A hierarchy of equivalences for asynchronous calculi, (Larsen, K. G.; Skyum, S.; Winskel, G., Proceedings of ICALP ’98. Proceedings of ICALP ’98, LNCS, 1443 (1998), Springer-Verlag: Springer-Verlag Berlin), 844-855 · Zbl 0909.03030
[13] Honda, K. 1992, Notes on soundness of a mapping from \(πν\); Honda, K. 1992, Notes on soundness of a mapping from \(πν\)
[14] Honda, K.; Tokoro, M., On asynchronous communication semantics, (Tokoro, M.; Nierstrasz, O.; Wegner, P., Object-Based Concurrent Computing 1991. Object-Based Concurrent Computing 1991, LNCS, 612 (1992), Springer-Verlag: Springer-Verlag Berlin), 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: 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, (Bauer, F. L.; Brauer, W.; Schwichtenberg, H., Logic and Algebra of Specification. Logic and Algebra of Specification, Series F: Computer and System Sciences, 94 (1993), Springer-VerlagNATO Advanced Study Institute: Springer-VerlagNATO Advanced Study Institute Berlin)
[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, (Kuich, W., Proceedings of ICALP ’92. Proceedings of ICALP ’92, LNCS, 623 (1992), Springer-Verlag: Springer-Verlag Berlin), 685-695 · Zbl 1425.68298
[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, (Montanari, U.; Sassone, V., Proceedings of CONCUR ’96. Proceedings of CONCUR ’96, LNCS, 1119 (1996), Springer-Verlag: Springer-Verlag Berlin), 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: ACM New York, p. 256-265
[26] Parrow, J.; Sjödin, P., Multiway synchronization verified with coupled simulation, (Cleaveland, R., Proceedings of CONCUR ’92. Proceedings of CONCUR ’92, LNCS, 630 (1992), Springer-Verlag: Springer-Verlag Berlin), 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: 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, (Roscoe, A. W., A Classical Mind: Essays in Honour of C.A.R. Hoare (1994), Prentice-Hall: Prentice-Hall Englewood Cliffs), 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, (Degano, P.; Gorrieri, R.; Marchetti-Spaccamela, A., Proceedings of ICALP ’97. Proceedings of ICALP ’97, LNCS, 1256 (1997), Springer-Verlag: Springer-Verlag Berlin), 303-313 · Zbl 0930.68035
[32] Thomsen, B.; Leth, L.; Kuo, T.-M., A Facile tutorial, (Montanari, U.; Sassone, V., Proceedings of CONCUR ’96. Proceedings of CONCUR ’96, LNCS, 1119 (1996), Springer-Verlag: Springer-Verlag Berlin), 278-298
[33] Victor, B.; Parrow, J., Constraints as processes, (Montanari, U.; Sassone, V., Proceedings of CONCUR ’96. Proceedings of CONCUR ’96, LNCS, 1119 (1996), Springer-Verlag: Springer-Verlag Berlin), 389-405 · Zbl 1514.68187
[34] Yoshida, N., Graph types for monadic mobile processes, (Chandru, V.; Vinay, V., Proceedings of FSTTCS ’96. Proceedings of FSTTCS ’96, LNCS, 1180 (1996), Springer-Verlag: Springer-Verlag Berlin), 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. 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.