×

zbMATH — the first resource for mathematics

Towards a unified approach to encodability and separation results for process calculi. (English) Zbl 1209.68336
Summary: We present a unified approach to evaluate the relative expressive power of process calculi. In particular, we identify a small set of criteria (that have already been somehow presented in the literature) that an encoding should satisfy to be considered a valid means for language comparison. We argue that the combination of such criteria is a valid proposal by noting that: (i) several well-known encodings appeared in the literature satisfy them; (ii) this notion is not trivial, because some known encodings do not satisfy all the criteria we have proposed; (iii) several well-known separation results can be formulated in terms of our criteria; and (iv) some widely believed (but never formally proved) separation results can be proved by using the criteria we propose. Moreover, the criteria defined induce general proof-techniques for separation results that can be easily instantiated to cover known case-studies.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX Cite
Full Text: DOI
References:
[1] Amadio, R.M.; Castellani, I.; Sangiorgi, D., On bisimulations for the asynchronous \(\pi\)-calculus, Theoretical computer science, 195, 2, 291-324, (1998) · Zbl 0915.68009
[2] Arun-Kumar, S.; Hennessy, M., An efficiency preorder for processes, Acta informatica, 29, 8, 737-760, (1992) · Zbl 0790.68039
[3] M. Baldamus, J. Parrow, B. Victor, Spi-calculus translated to pi-calculus preserving may-tests, in: Proceedings of LICS, IEEE Computer Society, 2004, pp. 22-31.
[4] M. Baldamus, J. Parrow, B. Victor, A fully abstract encoding of the π-calculus with data terms, in: Proceedings of ICALP, LNCS, vol. 3580, Springer, 2005, pp. 1202-1213. · Zbl 1085.68594
[5] Boreale, M., On the expressiveness of internal mobility in name-passing calculi, Theoretical computer science, 195, 2, 205-226, (1998) · Zbl 0915.68059
[6] G. Boudol, Asynchrony and the \(\pi\)-calculus (note), Rapport de Recherche 1702, INRIA Sophia-Antipolis, May 1992.
[7] M. Bugliesi, M. Giunti, Secure implementations of typed channel abstractions, in: Proceedings of POPL, ACM, 2007, pp. 251-262. · Zbl 1295.68078
[8] N. Busi, M. Gabbrielli, G. Zavattaro, Replication vs. recursive definitions in channel based calculi, in: Proceedings of ICALP’03, LNCS, vol. 2719, Springer, 2003, pp. 133-144. · Zbl 1039.68082
[9] N. Busi, M. Gabbrielli, G. Zavattaro, Comparing recursion, replication, and iteration in process calculi, in: Proceedings of ICALP’04, LNCS, vol. 3142, Springer, 2004, pp. 307-319. · Zbl 1098.68086
[10] D. Cacciagrano, F. Corradini, J. Aranda, F.D. Valencia, Linearity, persistence and testing semantics in the asynchronous pi-calculus, in: Proceedings of EXPRESS’07, ENTCS, vol. 194, No. 2, 2008, pp. 59-84. · Zbl 1277.68167
[11] Cacciagrano, D.; Corradini, F.; Palamidessi, C., Separation of synchronous and asynchronous communication via testing, Theoretical computer science, 386, 3, 218-235, (2007) · Zbl 1143.68051
[12] Carbone, M.; Maffeis, S., On the expressive power of polyadic synchronisation in pi-calculus, Nordic journal of computing, 10, 2, 70-98, (2003) · Zbl 1062.68077
[13] L. Cardelli, G. Ghelli, A.D. Gordon, Mobility types for mobile ambients, in: Proceedings of ICALP’99, vol. 1644, LNCS, Springer, 1999.
[14] Cardelli, L.; Ghelli, G.; Gordon, A.D., Types for the ambient calculus, Information and computation, 177, 2, 160-194, (2002) · Zbl 1093.68060
[15] L. Cardelli, A.D. Gordon, Types for mobile ambients, in: Proceedings of POPL’99, ACM, 1999, pp. 79-92.
[16] Cardelli, L.; Gordon, A.D., Mobile ambients, Theoretical computer science, 240, 1, 177-213, (2000) · Zbl 0954.68108
[17] de Boer, F.; Palamidessi, C., Embedding as a tool for language comparison, Information and computation, 108, 1, 128-157, (1994) · Zbl 0788.68014
[18] De Nicola, R.; Hennessy, M., Testing equivalence for processes, Theoretical computer science, 34, 83-133, (1984) · Zbl 0985.68518
[19] C. Fournet, G. Gonthier, The reflexive chemical abstract machine and the join-calculus, in: Proceedings of POPL’96, ACM, 1996, pp. 372-385.
[20] R.J. van Glabbeek, The linear time – branching time spectrum, in: Proceedings of CONCUR’90, vol. 458, LNCS, Springer, 1990, pp. 278-297.
[21] R.J. van Glabbeek, The linear time – branching time spectrum II; the semantics of sequential systems with silent moves, in: Proceedings of CONCUR’93, vol. 715, LNCS, Springer, 1993, pp. 66-81.
[22] D. Gorla, On the relative expressive power of ambient-based calculi, in: Proceedings of TGC’08, LNCS, vol. 5474, Springer, 2009, pp. 141-156.
[23] D. Gorla, On the relative expressive power of asynchronous communication primitives, in: Proceedings of FoSSaCS’06, LNCS, vol. 3921, Springer, 2006, pp. 47-62. · Zbl 1180.68190
[24] D. Gorla, On the relative expressive power of calculi for mobility, in: Proceedings of MFPS XXV, ENTCS, vol. 249, Elsevier, 2009, pp. 269-286. · Zbl 1337.68182
[25] D. Gorla, Synchrony vs asynchrony in communication primitives, in: Proceedings of EXPRESS’06, ENTCS, vol. 175, No. 3, Elsevier, 2007, pp. 87-108. · Zbl 1277.68185
[26] Gorla, D., Comparing communication primitives via their relative expressive power, Information and computation, 206, 8, 931-952, (2008) · Zbl 1169.68009
[27] D. Gorla, Towards a unified approach to encodability and separation results for process calculi, in: Proceedings of CONCUR’08, LNCS, vol. 5201, Springer, 2008, pp. 492-507. · Zbl 1160.68466
[28] B. Haagensen, S. Maffeis, I. Phillips, Matching systems for concurrent calculi, in: Proceedings of EXPRESS’07, ENTCS, vol. 194, No. 2, 2008, pp. 85-99. · Zbl 1277.68189
[29] Hennessy, M.; Riely, J., Resource access control in systems of mobile agents, Information and computation, 173, 82-120, (2002) · Zbl 1009.68081
[30] M. Herlihy, Impossibility and universality results for wait-free synchronization, in: Proceedings of PODC, ACM Press, 1988, pp. 276-290.
[31] K. Honda, M. Tokoro, An object calculus for asynchronous communication, in: Proceedings of ECOOP’91, LNCS, vol. 512, Springer, 1991, pp. 133-147.
[32] Honda, K.; Yoshida, N., On reduction-based process semantics, Theoretical computer science, 152, 2, 437-486, (1995) · Zbl 0871.68122
[33] C. Laneve, B. Victor, Solos in concert, in: Proceedings of ICALP’99, LNCS, vol. 1644, Springer, 1999, pp. 513-523.
[34] Levi, F., A typed encoding of boxed into safe ambients, Acta informatica, 42, 6, 429-500, (2006) · Zbl 1089.68021
[35] Merro, M.; Zappa Nardelli, F., Behavioral theory for mobile ambients, Journal of the ACM, 52, 6, 961-1023, (2005) · Zbl 1326.68201
[36] M. Merro, D. Sangiorgi, On asynchrony in name-passing calculi, in: Proceedings of ICALP’98, LNCS, vol. 1443, Springer, 1998, pp. 856-867. · Zbl 0910.03019
[37] Milner, R., Communication and concurrency, (1989), Prentice Hall · Zbl 0683.68008
[38] Milner, R., Functions as processes, Mathematical structures in computer science, 2, 2, 119-141, (1992) · Zbl 0773.03012
[39] R. Milner, The polyadic \(\pi\)-calculus: a tutorial, in: Logic and Algebra of Specification, Series F. NATO ASI, vol. 94, Springer, 1993.
[40] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, part I/II, Information and computation, 100, 1-77, (1992)
[41] R. Milner, D. Sangiorgi, Barbed bisimulation, in: Proceedings of ICALP’92, LNCS, vol. 623, Springer, 1992, pp. 685-695.
[42] Nestmann, U., What is a ‘good’ encoding of guarded choice?, Information and computation, 156, 287-319, (2000) · Zbl 1046.68625
[43] U. Nestmann, Welcome to the jungle: a subjective guide to mobile process calculi, in: Proceedings of CONCUR’06, LNCS, vol. 4137, Springer, 2006, pp. 52-63. · Zbl 1151.68548
[44] Nestmann, U.; Pierce, B.C., Decoding choice encodings, Information and computation, 163, 1-59, (2000) · Zbl 1003.68080
[45] Palamidessi, C., Comparing the expressive power of the synchronous and the asynchronous \(\pi\)-calculi, Mathematical structures in computer science, 13, 5, 685-719, (2003)
[46] C. Palamidessi, V.A. Saraswat, F.D. Valencia, B. Victor, On the expressiveness of linearity vs persistence in the asychronous pi-calculus, in: Proceedings of LICS, IEEE Computer Society, 2006, pp. 59-68.
[47] Palamidessi, C.; Valencia, F., Recursion vs replication in process calculi: expressiveness, Bulletin of the EATCS, 87, 105-125, (2005) · Zbl 1169.68551
[48] J. Parrow, Trios in concert, in: Proof, Language and Interaction: Essays in Honour of Robin Milner, Foundations of Computing, MIT Press, 2000, pp. 621-637.
[49] J. Parrow, Expressiveness of process algebras, in: Emerging Trends in Concurrency, ENTCS, vol. 209, 2008, pp. 173-186. · Zbl 1279.68264
[50] Phillips, I.; Vigliotti, M., Electoral systems in ambient calculi, Information and computation, 206, 1, 34-72, (2008) · Zbl 1133.68059
[51] Phillips, I.; Vigliotti, M., Leader election in rings of ambient processes, Theoretical computer science, 356, 3, 468-494, (2006) · Zbl 1092.68068
[52] Plotkin, G.D., A structural approach to operational semantics, Journal of logic and algebraic programming, 60-61, 17-139, (2004) · Zbl 1082.68062
[53] P. Quaglia, D. Walker, On synchronous and asynchronous mobile processes, in: Proceedings of FoSSaCS 2000, LNCS, vol. 1784, Springer, 2000, pp. 283-296. · Zbl 0961.68092
[54] Quaglia, P.; Walker, D., Types and full abstraction for polyadic pi-calculus, Information and computation, 200, 215-246, (2005) · Zbl 1101.68062
[55] J. Rathke, V. Sassone, P. Sobocinski, Semantic barbs and biorthogonality, in: Proceedings of FoSSaCS, LNCS, vol. 4423, Springer, 2007, pp. 302-316. · Zbl 1195.68073
[56] Sangiorgi, D., Bisimulation in higher-order process calculi, Information and computation, 131, 141-178, (1996) · Zbl 0876.68042
[57] Sangiorgi, D.; Walker, D., The \(\pi\)-calculus: A theory of mobile processes, (2001), Cambridge University Press · Zbl 0981.68116
[58] Vasconcelos, V., Processes, functions, and datatypes, Theory and practice of object systems, 5, 2, 97-110, (1999)
[59] N. Yoshida, Graph types for monadic mobile processes, in: Proceedings of FSTTCS’96, LNCS, vol. 1180, Springer, 1996, pp. 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.