Stronger Validity Criteria for Encoding Synchrony

  • Rob van GlabbeekEmail author
  • Ursula Goltz
  • Christopher Lippert
  • Stephan Mennicke
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11760)


We analyse two translations from the synchronous into the asynchronous \(\pi \)-calculus, both without choice, that are often quoted as standard examples of valid encodings, showing that the asynchronous \(\pi \)-calculus is just as expressive as the synchronous one. We examine which of the quality criteria for encodings from the literature support the validity of these translations. Moreover, we prove their validity according to much stronger criteria than considered previously in the literature.


Process calculi Expressiveness Translations Quality criteria for encodings Valid encoding Compositionality Operational correspondence Semantic equivalences Asynchronous \(\pi \)-calculus 


  1. 1.
    Amadio, R.M., Castellani, I., Sangiorgi, D.: On bisimulations for the asynchronous pi-calculus. Theoret. Comput. Sci. 195(2), 291–324 (1998). Scholar
  2. 2.
    Baldamus, M., Parrow, J., Victor, B.: A fully abstract encoding of the \({\pi }\)-calculus with data terms. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1202–1213. Springer, Heidelberg (2005). Scholar
  3. 3.
    Beauxis, R., Palamidessi, C., Valencia, F.D.: On the asynchronous nature of the asynchronous \(\pi \)-calculus. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 473–492. Springer, Heidelberg (2008). Scholar
  4. 4.
    Boudol, G.: Notes on algebraic calculi of processes. In: Apt, K.R. (eds) Logics and Models of Concurrent Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 13, pp. 261–303. Springer, Heidelberg (1985). Scholar
  5. 5.
    Boudol, G.: Asynchrony and the \(\pi \)-calculus (Note). Technical Report, 1702, INRIA (1992)Google Scholar
  6. 6.
    Brinksma, E., Rensink, A., Vogler, W.: Fair testing. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 313–327. Springer, Heidelberg (1995). Scholar
  7. 7.
    Cacciagrano, D., Corradini, F.: On synchronous and asynchronous communication paradigms. ICTCS 2001. LNCS, vol. 2202, pp. 256–268. Springer, Heidelberg (2001). Scholar
  8. 8.
    Cacciagrano, D., Corradini, F., Palamidessi, C.: Separation of synchronous and asynchronous communication via testing. Theoret. Comput. Sci. 386(3), 218–235 (2007). Scholar
  9. 9.
    De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoret. Comput. Sci. 34, 83–133 (1984). Scholar
  10. 10.
    Du, W., Yang, Z., Zhu, H.: A fully abstract encoding for sub asynchronous Pi calculus. In: Pang, J., Zhang, C., He, J., Weng, J. (eds.) Proceedings of TASE 2018, pp. 17–27. IEEE Computer Society Press (2018).
  11. 11.
    Fu, Y.: Theory of interaction. Theoret. Comput. Sci. 611, 1–49 (2016). Scholar
  12. 12.
    Given-Wilson, T.: Expressiveness via intensionality and concurrency. In: Ciobanu, G., Méry, D. (eds.) ICTAC 2014. LNCS, vol. 8687, pp. 206–223. Springer, Cham (2014). Scholar
  13. 13.
    Given-Wilson, T.: On the expressiveness of intensional communication. In: Borgström, J., Crafa, S. (eds.) Proceedings EXPRESS/SOS 2014. EPTCS, vol. 160, pp. 30–46 (2014). Scholar
  14. 14.
    Given-Wilson, T., Legay, A.: On the expressiveness of joining. In: Knight, S., Lanese, I., Lluch Lafuente, A., Torres Vieira, H. (eds.) Proceedings of ICE2015. EPTCS, vol. 189, pp. 99–113 (2015). Scholar
  15. 15.
    Given-Wilson, T., Legay, A.: On the expressiveness of symmetric communication. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 139–157. Springer, Cham (2016). Scholar
  16. 16.
    van Glabbeek, R.J.: On the expressiveness of ACP. In: Ponse, A., Verhoef, C., van Vlijmen, S.F.M. (eds.) Algebra of Communicating Processes. Workshops in Computing, pp. 188–217. Springer, London (1995), Scholar
  17. 17.
    van Glabbeek, R.J.: Musings on encodings and expressiveness. In: Luttik, B., Reniers, M.A. (eds.) Proceedings EXPRESS/SOS 2012. EPTCS, vol. 89, pp. 81–98 (2012). Scholar
  18. 18.
    van Glabbeek, R.J.: On the validity of encodings of the synchronous in the asynchronous \(\pi \)-calculus. Inf. Process. Lett. 137, 17–25 (2018). Scholar
  19. 19.
    van Glabbeek, R.J.: A Theory of Encodings and Expressiveness. Technical Report, Data61, CSIRO (2018). Full version of [20]
  20. 20.
    van Glabbeek, R.J.: A theory of encodings and expressiveness (extended abstract). In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 183–202. Springer, Cham (2018). Scholar
  21. 21.
    Gorla, D.: A taxonomy of process calculi for distribution and mobility. Distrib. Comput. 23(4), 273–299 (2010). Scholar
  22. 22.
    Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9), 1031–1053 (2010). Scholar
  23. 23.
    Gorla, D., Nestmann, U.: Full abstraction for expressiveness: history, myths and facts. Math. Struct. Comput. Sci. 26(4), 639–654 (2016). Scholar
  24. 24.
    Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 133–147. Springer, Heidelberg (1991). Scholar
  25. 25.
    Lanese, I., Pérez, J.A., Sangiorgi, D., Schmitt, A.: On the expressiveness of polyadic and synchronous communication in higher-order process calculi. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 442–453. Springer, Heidelberg (2010). Scholar
  26. 26.
    Milner, R.: The Polyadic \(\pi \)-Calculus: A Tutorial. Technical Report ECS-LFCS-91-180, The University of Edinburgh. Informatics Report Series (1991)Google Scholar
  27. 27.
    Milner, R.: Functions as processes. Math. Struct. Comput. Sci. 2(2), 119–141 (1992). Scholar
  28. 28.
    Natarajan, V., Cleaveland, R.: Divergence and fair testing. In: Fülöp, Z., Gécseg, F. (eds.) ICALP 1995. LNCS, vol. 944, pp. 648–659. Springer, Heidelberg (1995). Scholar
  29. 29.
    Nestmann, U.: What is a “Good” encoding of guarded choice? Inf. Comput. 156(1–2), 287–319 (2000). Scholar
  30. 30.
    Nestmann, U., Pierce, B.C.: Decoding choice encodings. Inf. Comput. 163(1), 1–59 (2000). Scholar
  31. 31.
    Palamidessi, C.: Comparing the expressive power of the synchronous and asynchronous pi-calculi. Math. Struct. Comput. Sci. 13(5), 685–719 (2003). Scholar
  32. 32.
    Parrow, J.: General conditions for full abstraction. Math. Struct. Comput. Sci. 26(4), 655–657 (2016). Scholar
  33. 33.
    Peters, K., van Glabbeek, R.J.: Analysing and comparing encodability criteria. In: Crafa, S., Gebler, D.E. (eds.) EXPRESS/SOS 2015. EPTCS, vol. 190, pp. 46–60 (2015). Scholar
  34. 34.
    Peters, K., Nestmann, U.: Is it a “Good” encoding of mixed choice? In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 210–224. Springer, Heidelberg (2012). Scholar
  35. 35.
    Peters, K., Nestmann, U., Goltz, U.: On distributability in process calculi. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 310–329. Springer, Heidelberg (2013). Scholar
  36. 36.
    Peters, K., Schicke, J.-W., Nestmann, U.: Synchrony vs causality in the asynchronous pi-calculus. In: Luttik, B., Valencia, F. (eds.) Proceedings EXPRESS 2011, EPTCS, vol. 64, pp. 89–103 (2011). Scholar
  37. 37.
    Quaglia, P., Walker, D.: On synchronous and asynchronous mobile processes. In: Tiuryn, J. (ed.) FoSSaCS 2000. LNCS, vol. 1784, pp. 283–296. Springer, Heidelberg (2000). Scholar
  38. 38.
    Riecke, J.G.: Fully abstract translations between functional languages. In: Wise, D.S. (ed.) Proceedings POPL 1991, pp. 245–254. ACM Press (1991).
  39. 39.
    Sangiorgi, D., Walker, D.: The \(\pi \)-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)Google Scholar
  40. 40.
    Shapiro, E.Y.: Separating concurrent languages with categories of language embeddings. In: Koutsougeras, C., Vitter, J.S. (eds.) STOC 1991, pp. 198–208. ACM (1991).
  41. 41.
    Shapiro, E.: Embeddings among concurrent programming languages. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 486–503. Springer, Heidelberg (1992). Scholar
  42. 42.
    de Simone, R.: Higher-level synchronising devices in Meije-SCCS. Theoret. Comput. Sci. 37, 245–267 (1985). Scholar
  43. 43.
    Vaandrager, F.W.: Expressiveness results for process algebras. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1992. LNCS, vol. 666, pp. 609–638. Springer, Heidelberg (1993). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Rob van Glabbeek
    • 1
    • 2
    Email author
  • Ursula Goltz
    • 3
  • Christopher Lippert
    • 3
  • Stephan Mennicke
    • 3
  1. 1.Data61, CSIROSydneyAustralia
  2. 2.Computer Science and EngineeringUniversity of New South WalesSydneyAustralia
  3. 3.Institute for Programming and Reactive SystemsTU BraunschweigBraunschweigGermany

Personalised recommendations