×

On the validity of encodings of the synchronous in the asynchronous \(\pi\)-calculus. (English) Zbl 1390.68490

Summary: Process calculi may be compared in their expressive power by means of encodings between them. A widely accepted definition of what constitutes a valid encoding for (dis)proving relative expressiveness results between process calculi was proposed by D. Gorla [Inf. Comput. 208, No. 9, 1031–1053 (2010; Zbl 1209.68336)]. Prior to this work, diverse encodability and separation results were generally obtained using distinct, and often incompatible, quality criteria on encodings.
Textbook examples of valid encoding are the encodings proposed by G. Boudol [Asynchrony and the \(\pi\)-calculus. Techn. Rep. 1702, INRIA (1992)] and by K. Honda and M. Tokoro [“An object calculus for asynchronous communication”, Lect. Notes Comput. Sci. 512, 133–147 (1991; doi:10.1007/BFb0057019)] of the synchronous choice-free \(\pi\)-calculus into its asynchronous fragment, illustrating that the latter is no less expressive than the former. Here I formally establish that these encodings indeed satisfy Gorla’s criteria.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Citations:

Zbl 1209.68336

Software:

LOTOS
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Austry, D.; Boudol, G., Algèbre de processus et synchronisations, Theor. Comput. Sci., 30, 1, 91-131, (1984) · Zbl 0533.68026
[2] Baldamus, M.; Parrow, J.; Victor, B., Spi calculus translated to π-calculus preserving may-tests, (Proc. LICS’04, (2004)), 22-31
[3] Bergstra, J. A.; Klop, J. W., Algebra of communicating processes, (Mathematics and Computer Science, CWI Monograph, vol. 1, (1986), North-Holland), 89-138 · Zbl 0605.68013
[4] Bolognesi, T.; Brinksma, E., Introduction to the ISO specification language LOTOS, Comput. Netw., 14, 25-59, (1987)
[5] Boreale, M., On the expressiveness of internal mobility in name-passing calculi, Theor. Comput. Sci., 195, 2, 205-226, (1998) · Zbl 0915.68059
[6] Boudol, G., Asynchrony and the π-calculus (note), (1992), INRIA, Tech. Rep. 1702
[7] Brinksma, E.; Rensink, A.; Vogler, W., Fair testing, (Proc. CONCUR’95, Lect. Notes Comput. Sci., vol. 962, (1995), Springer), 313-327
[8] Brookes, S. D.; Hoare, C. A.R.; Roscoe, A. W., A theory of communicating sequential processes, J. ACM, 31, 3, 560-599, (1984) · Zbl 0628.68025
[9] Busi, N.; Gabbrielli, M.; Zavattaro, G., On the expressive power of recursion, replication and iteration in process calculi, Math. Struct. Comput. Sci., 19, 6, 1191-1222, (2009) · Zbl 1191.68430
[10] Cacciagrano, D.; Corradini, F., On synchronous and asynchronous communication paradigms, (Proc. 7th Italian Conference on Theoretical Computer Science, ICTCS’01, Lect. Notes Comput. Sci., vol. 2202, (2001), Springer), 256-268 · Zbl 1042.68614
[11] Cacciagrano, D.; Corradini, F.; Aranda, J.; Valencia, F. D., Linearity, persistence and testing semantics in the asynchronous pi-calculus, Electron. Notes Theor. Comput. Sci., 194, 2, 59-84, (2008) · Zbl 1277.68167
[12] Cacciagrano, D.; Corradini, F.; Palamidessi, C., Separation of synchronous and asynchronous communication via testing, Theor. Comput. Sci., 386, 3, 218-235, (2007) · Zbl 1143.68051
[13] Carbone, M.; Maffeis, S., On the expressive power of polyadic synchronisation in pi-calculus, Nord. J. Comput., 10, 2, 70-98, (2003) · Zbl 1062.68077
[14] Cardelli, L.; Gordon, A. D., Mobile ambients, Theor. Comput. Sci., 240, 1, 177-213, (2000) · Zbl 0954.68108
[15] De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theor. Comput. Sci., 34, 83-133, (1984) · Zbl 0985.68518
[16] Given-Wilson, T., Expressiveness via intensionality and concurrency, (Proc. ICTAC’14, Lect. Notes Comput. Sci., vol. 8687, (2014)), 206-223 · Zbl 1432.68307
[17] Given-Wilson, T., On the expressiveness of intensional communication, (Proc. EXPRESS/SOS’14, EPTCS, vol. 160, (2014)), 30-46 · Zbl 1464.68247
[18] Given-Wilson, T.; Legay, A., On the expressiveness of joining, (Proc. ICE’15, EPTCS, vol. 189, (2015)), 99-113 · Zbl 1433.68253
[19] Given-Wilson, T.; Legay, A., On the expressiveness of symmetric communication, (Proc. ICTAC’16, Lect. Notes Comput. Sci., vol. 9965, (2016), Springer), 139-157 · Zbl 1482.68150
[20] van Glabbeek, R. J., On the expressiveness of ACP, (Proc. ACP’94, Workshops in Computing, (1994), Springer), 188-217
[21] van Glabbeek, R. J., Musings on encodings and expressiveness, (Proc. EXPRESS/SOS’12, EPTCS, vol. 89, (2012)), 81-98 · Zbl 1459.68149
[22] van Glabbeek, R. J., On the validity of encodings of the synchronous in the asynchronous pi-calculus, (2018), Technical Report, Data61 CSIRO. Full version of the current paper, available at · Zbl 1390.68490
[23] Gorla, D., A taxonomy of process calculi for distribution and mobility, Distrib. Comput., 23, 4, 273-299, (2010) · Zbl 1231.68169
[24] Gorla, D., Towards a unified approach to encodability and separation results for process calculi, Inf. Comput., 208, 9, 1031-1053, (2010) · Zbl 1209.68336
[25] Groote, J. F.; Mousavi, M. R., Modeling and analysis of communicating systems, (2014), MIT Press · Zbl 1353.68006
[26] Haagensen, B.; Maffeis, S.; Phillips, I., Matching systems for concurrent calculi, Electron. Notes Theor. Comput. Sci., 194, 2, 85-99, (2008) · Zbl 1277.68189
[27] Hatzel, M.; Wagner, C.; Peters, K.; Nestmann, U., Encoding CSP into CCS, (Proc. EXPRESS/SOS’15, EPTCS, vol. 190, (2015)), 61-75 · Zbl 1476.68173
[28] Honda, K.; Tokoro, M., An object calculus for asynchronous communication, (Proc. ECOOP’91, Lect. Notes Comput. Sci., vol. 512, (1991), Springer), 133-147
[29] Lanese, I.; Pérez, J. A.; Sangiorgi, D.; Schmitt, A., On the expressiveness of polyadic and synchronous communication in higher-order process calculi, (Proc ICALP’10, Lect. Notes Comput. Sci., vol. 6199, (2010)), 442-453 · Zbl 1288.68183
[30] Milner, R., A calculus of communicating systems, Lect. Notes Comput. Sci., vol. 92, (1980), Springer · Zbl 0452.68027
[31] Milner, R., Calculi for synchrony and asynchrony, Theor. Comput. Sci., 25, 267-310, (1983) · Zbl 0512.68026
[32] Milner, R., Functions as processes, Math. Struct. Comput. Sci., 2, 2, 119-141, (1992) · Zbl 0773.03012
[33] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, part I + II, Inf. Comput., 100, 1, 1-77, (1992) · Zbl 0752.68037
[34] Natarajan, V.; Cleaveland, R., Divergence and fair testing, (Proc. ICALP’95, Lect. Notes Comput. Sci., vol. 944, (1995), Springer), 648-659 · Zbl 1412.68155
[35] Nestmann, U., What is a “good” encoding of guarded choice?, Inf. Comput., 156, 1-2, 287-319, (2000) · Zbl 1046.68625
[36] Nestmann, U.; Pierce, B. C., Decoding choice encodings, Inf. Comput., 163, 1, 1-59, (2000) · Zbl 1003.68080
[37] Palamidessi, C., Comparing the expressive power of the synchronous and asynchronous pi-calculi, Math. Struct. Comput. Sci., 13, 5, 685-719, (2003)
[38] Palamidessi, C.; Saraswat, V. A.; Valencia, F. D.; Victor, B., On the expressiveness of linearity vs persistence in the asychronous pi-calculus, (Proc. LICS’06, (2006), IEEE Computer Society Press), 59-68
[39] Palamidessi, C.; Valencia, F. D., Recursion vs replication in process calculi: expressiveness, Bull. Eur. Assoc. Theor. Comput. Sci., 87, 105-125, (2005) · Zbl 1169.68551
[40] Parrow, J., Trios in concert, (Proof, Language, and Interaction, Essays in Honour of Robin Milner, (2000), The MIT Press), 623-638 · Zbl 0968.68018
[41] Peters, K.; van Glabbeek, R. J., Analysing and comparing encodability criteria, (EXPRESS/SOS’15, EPTCS, vol. 190, (2015)), 46-60 · Zbl 1476.68181
[42] Peters, K.; Nestmann, U., Is it a “good” encoding of mixed choice?, (Proc. FoSSaCS’12, Lect. Notes Comput. Sci., vol. 7213, (2012)), 210-224 · Zbl 1352.68190
[43] Peters, K.; Nestmann, U., Breaking symmetries, Math. Struct. Comput. Sci., 26, 6, 1054-1106, (2016) · Zbl 1362.68219
[44] Peters, K.; Nestmann, U.; Goltz, U., On distributability in process calculi, (Proc. ESOP’13, Lect. Notes Comput. Sci., vol. 7792, (2013)), 310-329 · Zbl 1381.68215
[45] Peters, K.; Schicke, J.-W.; Nestmann, U., Synchrony vs causality in the asynchronous pi-calculus, (Proc. EXPRESS’11, EPTCS, vol. 64, (2011)), 89-103 · Zbl 1457.68192
[46] Phillips, I.; Vigliotti, M. G., Leader election in rings of ambient processes, Theor. Comput. Sci., 356, 3, 468-494, (2006) · Zbl 1092.68068
[47] Phillips, I.; Vigliotti, M. G., Symmetric electoral systems for ambient calculi, Inf. Comput., 206, 1, 34-72, (2008) · Zbl 1133.68059
[48] Quaglia, P.; Walker, D., On synchronous and asynchronous mobile processes, (Proc. FoSSaCS’00, Lect. Notes Comput. Sci., vol. 1784, (2000), Springer), 283-296 · Zbl 0961.68092
[49] Sangiorgi, D., From π-calculus to higher-order π-calculus — and back, (Proc. TAPSOFT’93, Lect. Notes Comput. Sci., vol. 668, (1993)), 151-166 · Zbl 1497.68351
[50] Sangiorgi, D.; Walker, D., The π-calculus: A theory of mobile processes, (2001), Cambridge University Press · Zbl 0981.68116
[51] de Simone, R., Higher-level synchronising devices in meije-SCCS, Theor. Comput. Sci., 37, 245-267, (1985) · Zbl 0598.68027
[52] Vaandrager, F. W., Expressiveness results for process algebras, (Proc. REX Workshop on Semantics: Foundations and Applications, Lect. Notes Comput. Sci., vol. 666, (1993), Springer), 609-638
[53] Versari, C.; Busi, N.; Gorrieri, R., An expressiveness study of priority in process calculi, Math. Struct. Comput. Sci., 19, 6, 1161-1189, (2009) · Zbl 1191.68447
[54] Vigliotti, M. G.; Phillips, I.; Palamidessi, C., Tutorial on separation results in process calculi via leader election problems, Theor. Comput. Sci., 388, 1-3, 267-289, (2007) · Zbl 1143.68056
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.