×

Distinguishing and relating higher-order and first-order processes by expressiveness. (English) Zbl 1276.68129

This paper compares the expressive power of higher-order and first-order process calculi. To this end, the process-passing and the name-passing paradigms are formally related. It presents the following results:
– first-order pi-calculus can faithfully express basic higher-order pi-calculus, even when enriched with a relabelling operator;
– basic higher-order pi-calculus cannot interpret first-order pi-calculus reasonably;
An encoding from first-order pi-calculus to basic higher-order pi-calculus enriched with a relabelling operator is also revisited and discussed.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baeten, J.: Branching bisimilarity is an equivalence indeed. Inform. Process. Lett. 58, 141–147 (1996) · Zbl 0875.68624 · doi:10.1016/0020-0190(96)00034-8
[2] Bundgaard, M., Godskesen, J.C., Hildebrandt, T.: Encoding the pi-calculus in higher-order calculi. Tech. Rep. TR-2008-106, IT University of Copenhagen (2008) · Zbl 1272.68293
[3] Bundgaard, M., Hildebrandt, T., Godskesen, J.C.: A cps encoding of name-passing in higher-order mobile embedded resources. Theor. Comput. Sci. 356, 422–439 (2006) · Zbl 1092.68064 · doi:10.1016/j.tcs.2006.02.006
[4] Busi, N., Gabbrielli, M., Zavattaro, G.: Replication vs recursive definitions in channel based calculi. In: Proceedings of ICALP 2003, LNCS, vol. 2719, pp. 133–144. Springer, Berlin (2003) · Zbl 1039.68082
[5] Busi, N., Gabbrielli, M., Zavattaro, G.: Comparing recursion, replication and iteration in process calculi. In: Proceedings of ICALP04, LNCS, vol. 3142, pp. 307–319. Springer, Berlin (2004) · Zbl 1098.68086
[6] Castagnaa, G., Vitekb, J., Nardelli, F.Z.: The seal calculus. Inform. Comput. 201(1), 1–54 (2005) · Zbl 1101.68060 · doi:10.1016/j.ic.2004.11.005
[7] Engberg, U.H., Nielsen, M.: A calculus of communicating systems with label passing. Tech. Rep. DAIMI PB-208, Computer Science Department, University of Aarhus (1986). http://www.daimi.aau.dk/PB/208/
[8] Engberg, U.H., Nielsen, M.: A calculus of communicating systems with label passing–ten years after. In: Proof, language, and interaction: essays in honour of Robin Milner, pp. 599–622. MIT Press, Cambridge (2000)
[9] Fu, Y.: Checking equivalence for higher order processes (2005). BASICS ( http://basics.sjtu.edu.cn ) Shanghai Jiao Tong University
[10] Fu, Y.: On quasi open bisimulation. Theor. Comput. Sci. 338(1–3), 96–126 (2005) · Zbl 1077.68060 · doi:10.1016/j.tcs.2004.10.041
[11] Fu, Y.: Theory of interaction (2009). BASICS ( http://basics.sjtu.edu.cn ) Shanghai Jiao Tong University
[12] Fu, Y., Lu, H.: On the expressiveness of interaction. Theor. Comput. Sci. 411, 1387–1451 (2010) · Zbl 1191.68436 · doi:10.1016/j.tcs.2009.11.011
[13] Fu, Y., Zhu, H.: Theory of name passing calculus (2009). BASICS ( http://basics.sjtu.edu.cn ) Shanghai Jiao Tong University
[14] Glabeek, R.: The linear time-branching time spectrum ii. In: Proceedings of CONCUR, LNCS, vol. 715, pp. 66–81. Springer, Berlin (1993)
[15] Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. In: Proceedings of CONCUR’ 08, LNCS, vol. 5201, pp. 492–507. Springer, Berlin (2008) · Zbl 1160.68466
[16] Hildebrandt, T., Godskesen, J.C., Bundgaard, M.: Bisimulation congruences for Homer–a calculus of higher order mobile embedded resources. Tech. Rep. TR-2004-52, IT University of Copenhagen (2004) · Zbl 1272.68293
[17] Lanese, I., Perez, J., Sangiorgi, D., Schmitt, A.: On the expressiveness and decidability of higher-order process calculi. In: Proceedings of the 23rd annual IEEE symposium on logic in computer science (LICS 2008), pp. 145–155. IEEE Computer Society (2008). Journal version in [22]
[18] Lanese, I., Pérez, J.A., Sangiorgi, D., Schmitt, A.: On the expressiveness and decidability of higher-order process calculi. Inform. Comput. 209(2), 198–226 (2010) · Zbl 1238.68100 · doi:10.1016/j.ic.2010.10.001
[19] Lanese, I., Pérez, J.A., Sangiorgi, D., Schmitt, A.: On the expressiveness of polyadic and synchronous communication in higher-order process calculi. In: Proceedings of ICALP 2010, LNCS, pp. 442–453. Springer, Berlin (2010) · Zbl 1288.68183
[20] Milner, R.: Communication and Concurrency. Prentice Hall, New Jersey (1989) · Zbl 0683.68008
[21] Milner, R.: Functions as processes. J. Math. Struct. Comput. Sci. 2(2), 119–141, : Research Report 1154. INRIA, Sofia Antipolis (1992). 1990 · Zbl 0773.03012
[22] Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes (parts i and ii). Inform. Comput. 100(1), 1–77 (1992) · Zbl 0752.68036 · doi:10.1016/0890-5401(92)90008-4
[23] Milner, R., Sangiorgi, D.: Barbed bisimulation. In: Proceedings 19-the International Colloquium on Automata, Languages and Programming (ICALP ’92), LNCS, Vol. 623, pp. 685–695. Springer, Berlin (1992)
[24] Nestmann, U., Pierce, B.: Decoding choice encodings. In: Proceedings of CONCUR 1996, LNCS, vol. 1119, pp. 179–194. Springer, Berlin (1996) · Zbl 1003.68080
[25] Palamidessi, C.: Comparing the expressive power of the synchronous and the asynchronous pi-calculus. Math. Struct. Comput. Sci. 13, 685–719 (2003) · doi:10.1017/S0960129503004043
[26] Palamidessi, C., Saraswat, V., Valencia, F.D., Victor, B.: On the expressiveness of linearity vs. persistence in the asychronous pi-calculus. In: Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS’06), pp. 59–68. IEEE Computer Society (2006)
[27] Plotkin, G.: A structural approach to operational semantics. Tech. Rep. DAIMI FN-19, Aarhus Universitetsforlag (1981)
[28] Pous, D.: Up-to techniques for weak bisimulation. In: Proceedings of International Colloquium on Automata, Languages and Programming (ICALP 2005), LNCS, Vol. 3580, pp. 730–741. Springer, Berlin (2005) · Zbl 1084.68085
[29] Sangiorgi, D.: Expressing mobility in process algebras: first-order and higher-order paradigms. Ph.d. thesis, University of Edinburgh (1992)
[30] Sangiorgi, D.: From $$\(\backslash\)pi $$ -calculus to higher-order $$\(\backslash\)pi $$ -calculus–and back. In: Proceedings TAPSOFT ’93, LNCS, Vol. 668, pp. 151–166. Springer, Berlin (1992)
[31] Sangiorgi, D.: Bisimulation for higher-order process calculi. Inform. Comput. 131(2), 141–178 (1996) · Zbl 0876.68042 · doi:10.1006/inco.1996.0096
[32] Sangiorgi, D.: Pi-calculus, internal mobility and agent-passing calculi. Theor. Comput. Sci. 167(2) (1996) · Zbl 0874.68103
[33] Sangiorgi, D.: A theory of bisimulation for $$\(\backslash\)pi $$ -calculus. Acta Informatica 33(1), 69–97 (1996) · Zbl 0835.68072 · doi:10.1007/s002360050036
[34] Sangiorgi, D.: On the bisimulation proof method. Math. Struct. Comput. Sci. 8(6), 447–479 (1998) · Zbl 0916.68057 · doi:10.1017/S0960129598002527
[35] Sangiorgi, D., Milner, R.: The problem of weak bisimulation up-to. In: Proceedings of CONCUR’92, LNCS, vol. 630, pp. 32–46. Springer, Berlin (1992)
[36] Sangiorgi, D., Walker, D.: On barbed equivalences in pi-calculus. In: Proceedings of CONCUR’01, LNCS, vol. 2154, pp. 292–304. Springer, Berlin (2001) · Zbl 1006.68090
[37] Sangiorgi, D., Walker, D.: The Pi-calculus: a Theory of Mobile Processes. Cambridge Universtity Press, Cambridge (2001) · Zbl 0981.68116
[38] Schmitt, A., Stefani, J.B.: The m-calculus: A higher-order distributed process calculus. In: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 50–61. ACM (2003) · Zbl 1321.68365
[39] Schmitt, A., Stefani, J.B.: The kell calculus: A family of higher-order distributed process calculi. In: Proceedings of the International Workshop on Global Computing 2004 Workshop (GC 2004), pp. 146–178. Springer, Berlin (2004) · Zbl 1111.68547
[40] Thomsen, B.: Calculi for higher order communicating systems. Ph.d. thesis, Department of Computing, Imperial College (1990)
[41] Thomsen, B.: Plain chocs, a second generation calculus for higher-order processes. Acta Informatica 30(1), 1–59 (1993) · Zbl 0790.68069 · doi:10.1007/BF01200262
[42] van Glabbeek, R.: What is branching time semantics and why to use it? In: G. Paun, G. Rozenberg, A. Salomaa (eds.) Current trends in theoretical computer science; entering the 21th century, pp. 469–479. World Scientific (1994)
[43] van Glabbeek, R.: Linear time-branching time spectrum i. In: Handbook of process algebra, pp. 3–99. North-Holland (2001) · Zbl 1035.68073
[44] van Glabbeek, R., Luttik, B., Trčka, N.: Branching bisimilarity with explicit divergence. Fundamenta Informaticae 93, 371–392 (2009) · Zbl 1183.68404
[45] van Glabbeek, R., Weijland, W.: Branching time and abstraction in bisimulation semantics. In: Information processing’89, pp. 613–618. North-Holland (1989) · Zbl 0882.68085
[46] Xu, X.: On the bisimulation theory and axiomatization of higher-order process calculi. Ph.D. thesis, BASICS, Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai, China, P.R. (2008)
[47] Xu, X.: Expressing first-order $$\(\backslash\)pi $$ -calculus in higher-order calculus of communicating systems. J. Comput. Sci. Technol. 24(1), 122–137 (2009) · Zbl 05672110 · doi:10.1007/s11390-009-9210-y
[48] Xu, X.: On bisimulation theory in linear higher-order pi-calculus. Trans. Petri Nets Other Models Concurr. III(5800), 244–274 (2009) · Zbl 1266.68139 · doi:10.1007/978-3-642-04856-2_10
[49] Yin, Q., Long, H.: Process passing calculus, revisited. J. Shanghai Jiao Tong Univ. (Sci.) (2012). To appear
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.