Using session types for reasoning about boundedness in the \(\pi \)-calculus

Acta Informatica volume 57, pages801–827(2020)Cite this article

Abstract

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.

Access options

Buy single article

Instant access to the full article PDF.

US$ 39.95

Tax calculation will be finalised during checkout.

References

  1. 1.

    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)

    MathSciNet  MATH  Google Scholar 

  2. 2.

    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)

    Google Scholar 

  3. 3.

    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

  4. 4.

    Dam, M.: Model checking mobile processes. Inf. Comput. 129(1), 35–51 (1996). https://doi.org/10.1006/inco.1996.0072

    MathSciNet  Article  MATH  Google Scholar 

  5. 5.

    D’Osualdo, E., Ong, L.: A type system for proving depth boundedness in the pi-calculus. CoRR (2015). arXiv:1502.00944

  6. 6.

    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

    MathSciNet  Article  MATH  Google Scholar 

  7. 7.

    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

  8. 8.

    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

  9. 9.

    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

  10. 10.

    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

    MathSciNet  Article  MATH  Google Scholar 

  11. 11.

    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

  12. 12.

    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

  13. 13.

    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)

  14. 14.

    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

    MathSciNet  Article  MATH  Google Scholar 

  15. 15.

    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

    MathSciNet  Article  MATH  Google Scholar 

  16. 16.

    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

    Article  MATH  Google Scholar 

  17. 17.

    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

Download references

Author information

Affiliations

  1. Department of Computer Science, Aalborg University, Aalborg, Denmark

    Hans Hüttel

Authors
  1. Hans Hüttel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hans Hüttel.

Additional information

Publisher's Note

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.

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

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

Download citation