The \(\pi \)-calculus is a well-established theoretical framework for describing mobile and parallel computation using name passing, and a central notion here is that of name binding. Unfortunately, non-trivial properties of \(\pi \)-calculus processes such as termination and bisimilarity are undecidable as a consequence of the fact that the calculus is Turing-powerful. The classes of depth-bounded and name-bounded processes are classes of \(\pi \)-calculus processes that impose constraints on how name binding is used in a process. A consequence of this is that some of the important decision problems that are undecidable for the full calculus now become decidable. However, membership of these classes of processes is undecidable, so it is difficult to make use of the positive decidability results in practice. In this paper we use binary session types to devise two type systems that give a sound and decidable characterization of each of these two properties. If a process is well-typed in our first system, it is depth-bounded. If a process is well-typed in our second, more restrictive type system, it will also be name-bounded.
This is a preview of subscription content, access via your institution.
Buy single article
Instant access to the full article PDF.
Tax calculation will be finalised during checkout.
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
Tax calculation will be finalised during checkout.
Amadio, R.M., Meyssonnier, C.: On decidability of the control reachability problem in the asynchronous pi-calculus. Nordic J. Comput. 9(2), 70–101 (2002)
Bernardi, G., Dardha, O., Gay, S.J., Kouzapas, D.: On duality relations for session types. In: Maffei, M., Tuosto, E. (eds.) Trustworthy Global Computing, pp. 51–66. Springer, Berlin (2014)
Caires, L: Behavioral and spatial observations in a logic for the pi-calculus. In: Walukiewicz, I (ed.) Proceedings of FOSSACS 2004, LNCS 2987, pp. 72–89, Springer, Berlin. https://doi.org/10.1007/978-3-540-24727-2_7
Dam, M.: Model checking mobile processes. Inf. Comput. 129(1), 35–51 (1996). https://doi.org/10.1006/inco.1996.0072
D’Osualdo, E., Ong, L.: A type system for proving depth boundedness in the pi-calculus. CoRR (2015). arXiv:1502.00944
Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Inf. 42(2–3), 191–225 (2005). https://doi.org/10.1007/s00236-005-0177-z
Graversen, E.F., Harbo, J.B., Hüttel, H., Bjerregaard, M.O., Poulsen, N.S., Wahl, S.: Type inference for session types in the \(\pi \)-calculus. In: Hildebrandt, T., Ravara, A., van der Werf, J., Weidlich, M. (eds.) Proceedings of WS-FM 2014 and WS-FM/BEAT 2015, LNCS 9421, Springer, Berlin (2015). https://doi.org/10.1007/978-3-319-33612-1_7
Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Proceedings of ESOP’98, pp. 122–138 (1998). https://doi.org/10.1007/BFb0053567
Hüchting, R., Majumdar, R., Meyer, R.: A Theory of Name Boundedness, pp. 182–196. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-40184-8_14
Lanese, I., Pérez, J.A., Sangiorgi, D., Schmitt, A.: On the expressiveness and decidability of higher-order process calculi. Inf. Comput. 209(2), 198–226 (2011). https://doi.org/10.1016/j.ic.2010.10.001
Lange, J., Ng, N., Toninho, B., Yoshida, N.: Fencing off Go: Liveness and safety for channel-based programming. In: POPL 2017, pp. 748–761. ACM, New York (2017). https://doi.org/10.1145/3009837
Meyer, R.: On boundedness in depth in the pi-calculus. In: Ausiello, G., Karhumäki, J., Mauri, G., Luke Ong, C.-H. (eds.) Proceedings of TCS 2008, Volume 273 of IFIP, pp. 477–489. Springer, Berlin (2008). https://doi.org/10.1007/978-0-387-09680-3_32
Meyer, R., Gorrieri, R.: On the relationship between \(\pi \)-calculus and finite place/transition Petri nets. In: Bravetti, M., Zavattaro, G. (eds.) Proceedings of CONCUR 2009. LNCS, Vol. 5710, pp. 463–480. Springer, Heidelberg (2009)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I. Inf. Comput. 100(1), 1–40 (1992). https://doi.org/10.1016/0890-5401(92)90008-4
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, II. Inf. Comput. 100(2), 41–77 (1992). https://doi.org/10.1016/0890-5401(92)90009-5
Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455–495 (1982). https://doi.org/10.1145/357172.357178
Wies, T., Zufferey, D., Henzinger, T.A.: Forward analysis of depth-bounded processes. In: Luke Ong (ed.) Proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’10), pp. 94–108. Springer, Berlin. https://doi.org/10.1007/978-3-642-12032-9_8
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
The paper is an expanded version of the paper with the same title that was presented at EXPRESS/SOS 2017 (Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics). The present version contains revised definitions and proofs of major results.
About this article
Cite this article
Hüttel, H. Using session types for reasoning about boundedness in the \(\pi \)-calculus. Acta Informatica 57, 801–827 (2020). https://doi.org/10.1007/s00236-019-00339-5