×

zbMATH — the first resource for mathematics

Decoding choice encodings. (English) Zbl 1003.68080
Summary: We study two encodings of the asynchronous \(\pi\)-calculus with input-guarded choice into its choice-free fragment. One encoding is divergence-free, but refines the atomic commitment of choice into gradual commitment. The other preserves atomicity, but introduces divergence. The divergent encoding is fully abstract with respect to weak bisimulation, but the more natural divergence-free encoding is not. Instead, we show that it is fully abstract with respect to coupled simulation, a slightly coarser – but still coinductively defined – equivalence that does not enforce bisimilarity of internal branching decisions. The correctness proofs for the two choice encodings introduce a novel proof tech- nique exploiting the properties of explicit decodings from translations to source terms.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
Pict
PDF BibTeX Cite
Full Text: DOI
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.; Leth, L.; Thomsen, B., From a concurrent λ-calculus to the π-calculus, (), 106-115
[4] Amadio, R.M., On the reduction of CHOCS bisimulation to π-calculus bisimulation, (), 112-126
[5] Amadio, R.M., Technical report, (Feb. 1994)
[6] Busi, N.; Gorrieri, R., Distributed conflicts in communicating systems, (), 49-65
[7] Boudol, G., Asynchrony and the π-calculus (note), Rapport de recherche, (May 1992)
[8] Buth, K.-H., Simulation of SOS definitions with term rewriting systems, (), 150-164
[9] Fournet, C.; Gonthier, G., The reflexive chemical abstract machine and the join-calculus, (), 372-385
[10] Gammelgaard, A., Internal report, (Dec. 1991)
[11] Glabbeek, R., The linear time – branching time spectrum II: the semantics of sequential systems with silent moves (extended abstract), (), 66-81
[12] Gladstein, D., Compiler correctness for concurrent languages, (Dec. 1994), Northeastern University
[13] Honda, K., CS report, (1992)
[14] Honda, K.; Tokoro, M., An object for asynchronous communication, (), 133-147
[15] Honda, K.; Tokoro, M., On asynchronous communication semantics, (), 21-51
[16] Honda, K.; Yoshida, N., Combinatory representation of mobile processes, Proceedings of POPL’94, (1994), Assoc. Comput. Mach New York, p. 348-360
[17] Honda, K.; Yoshida, N., Replication in concurrent combinators, (), 786-805 · Zbl 0942.03510
[18] Honda, K.; Yoshida, N., On reduction-based process semantics, Theoret. comput. sci., (1995), p. 437-486 · Zbl 0871.68122
[19] Jones, C., A pi-calculus semantics for an object-based design notation, (), 158-172
[20] Knabe, F., A distributed protocol for channel-based communication with choice, Comput. artificial intell., 12, 475-490, (1993)
[21] Lavatelli, C., Technical report, (Sept. 1993)
[22] Li, W., An operational approach to semantics and translation for concurrent programming languages, (Jan. 1983), University of EdinburghLFCS
[23] Li, B.Z., A π-calculus specification of prolog, (), 379-393
[24] Leth, L.; Thomsen, B., Some facile chemistry, Formal aspects comput., 7, 314-328, (1995)
[25] Millington, M., Theories of translation correctness for concurrent programming languages, Lfcs, (Aug. 1987), University of Edinburgh
[26] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs · Zbl 0683.68008
[27] Milner, R., Functions as processes, J. math. structures comput. sci., 2, 119-141, (1992) · Zbl 0773.03012
[28] Milner, R., The polyadic π-calculus: A tutorial, ()
[29] Mitchell, K., Implementations of process synchronisation and their analysis, Lfcs, (July 1986), University of Edinburgh
[30] Montanari, U.; Pistore, M., Concurrent semantics for the π-calculus, ()
[31] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, part I/II, Inform. and comput., 100, 1-77, (1992)
[32] Milner, R.; Sangiorgi, D., Barbed bisimulation, (), 685-695
[33] Montanari, U.; Sassone, V., Dynamic congruence vs. progressing bisimulation for CCS, Fund. inform., XVI, 171-199, (1992) · Zbl 0762.68044
[34] Nestmann, U., On determinacy and nondeterminacy in concurrent programming, (November 1996), Universität ErlangenTechnische Fakultät
[35] Nestmann, U., What is a “good” encoding of guarded choice?, () · Zbl 0911.68096
[36] Niehren, J., Functional computation as concurrent computation, Proceedings of POPL’96, (1996), Assoc. Comput New York, p. 333-343
[37] Odersky, M., Applying π: towards a basis for concurrent imperative programming, (), 95-108
[38] Odersky, M., Polarized name passing, (), 324-337 · Zbl 1354.68201
[39] Oostrom, V.; Raamsdonk, F., Comparing combinatory reduction systems and higher-order rewrite systems, (), 276-304
[40] Palamidessi, C., Comparing the expressive power of the synchronous and the asynchronous π-calculus, Proceedings of POPL’97, (1997), Assoc. Comput. Mach New York, p. 256-265
[41] Parrow, J., Trios in concert, ()
[42] Priese, L., On the concept of simulation in asynchronous, concurrent systems, Progress in cybernetics and systems research, (1978), p. 82-82
[43] Parrow, J.; Sjödin, P., Multiway synchronization verified with coupled simulation, (), 518-533
[44] Parrow, J.; Sjödin, P., The complete axiomatization of cs-congruence, (), 557-568 · Zbl 0941.68573
[45] Pierce, B.C.; Turner, D.N., Concurrent objects in a process calculus, (), 187-215
[46] Pierce, B.C.; Turner, D.N., Pict: A programming language based on the pi-calculus, ()
[47] Ross, B., A π-calculus semantics of logical variables and unification, (), 216-230
[48] Sangiorgi, D., From π-calculus to higher-order π-calculus—and back, (), 151-166
[49] Sangiorgi, D., An investigation into functions as processes, (), 143-159
[50] Sangiorgi, D., The lazy lambda calculus in a concurrency scenario, Inform. and comput., 111, 120-131, (1994) · Zbl 0804.03008
[51] Singiorgi, D., Rapport de recherche, (1995)
[52] Sangiorgi, D., On the bisimulation proof method, (), 479-488 · Zbl 1193.68177
[53] Sangiorgi, D., π-calculus, internal mobility and agent-passing calculi, Theoret. comput. sci., 167, 235-275, (1996) · Zbl 0874.68103
[54] Smolka, G., A foundation for higher-order concurrent constraint programming, (), 50-72
[55] Thomsen, B., Plain CHOCS. A second generation calculus for higher order processes, Acta inform., 30, 1-59, (1993) · Zbl 0790.68069
[56] Thomsen, B., A theory of higher order communicating systems, Inform. and comput., 116, 38-57, (1995) · Zbl 0823.68061
[57] Vaandrager, F., Process algebra semantics of POOL, (), 173-236
[58] Victor, B.; Parrow, J., Constraints as processes, (), 389-405
[59] Walker, D., Bisimulation and divergence, Inform. and comput., 85, 202-241, (1990) · Zbl 0713.68036
[60] Walker, D., π-calculus semantics of object-oriented programming languages, (), 532-547
[61] Walker, D., Some results on the π-calculus, (), 21-35
[62] Walker, D., Process calculus and parallel object-oriented programming languages, (), 369-390
[63] Walker, D., Algebraic proofs of properties of objects, (), 501-516
[64] Walker, D., Objects in the π-calculus, Inform. and comput., 116, 253-271, (1995) · Zbl 0828.68043
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.