Bounds on Mobility

  • Reiner Hüchting
  • Rupak Majumdar
  • Roland Meyer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)


We study natural semantic fragments of the π-calculus: depth-bounded processes (there is a bound on the longest communication path), breadth-bounded processes (there is a bound on the number of parallel processes sharing a name), and name-bounded processes (there is a bound on the number of shared names). We give a complete characterization of the decidability frontier for checking if a π-calculus process in one subclass belongs to another. Our main construction is a general acceleration scheme for π-calculus processes. Based on this acceleration, we define a Karp and Miller (KM) tree construction for the depth-bounded π-calculus. The KM tree can be used to decide if a depth-bounded process is name-bounded, if a depth-bounded process is breadth-bounded by a constant k, and if a name-bounded process is additionally breadth-bounded. Moreover, we give a procedure that decides whether an arbitrary process is bounded in depth by a given k.

We complement our positive results with undecidability results for the remaining cases. While depth- and name-boundedness are known to be Σ1-complete, we show that breadth-boundedness is Σ2-complete, and checking if a process has a breadth bound at most k is Π1-complete, even when the input process is promised to be breadth-bounded.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103–115. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  2. 2.
    Dufourd, C., Jančar, P., Schnoebelen, P.: Boundedness of reset P/T nets. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 301–310. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: LICS, pp. 70–80 (June 1998)Google Scholar
  4. 4.
    Finkel, A.: A generalization of the procedure of Karp and Miller to well structured transition systems. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 499–508. Springer, Heidelberg (1987)CrossRefGoogle Scholar
  5. 5.
    Finkel, A.: Reduction and covering of infinite reachability trees. Inf. Comp. 89(2), 144–179 (1990)CrossRefzbMATHGoogle Scholar
  6. 6.
    Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part I: Completions. In: STACS, pp. 433–444 (2009)Google Scholar
  7. 7.
    Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part II: Complete WSTS. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 188–199. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  8. 8.
    Finkel, A., Goubault-Larrecq, J.: The theory of WSTS: The case of complete WSTS. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol. 7347, pp. 3–31. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  9. 9.
    Hüchting, R., Majumdar, R., Meyer, R.: A theory of name boundedness. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 182–196. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  10. 10.
    Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)CrossRefzbMATHMathSciNetGoogle Scholar
  11. 11.
    Meyer, R.: On boundedness in depth in the π-calculus. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds.) IFIP TCS. IFIP, vol. 273, pp. 477–489. Springer, Heidelberg (2008)Google Scholar
  12. 12.
    Meyer, R.: A theory of structural stationarity in the π-calculus. Acta Inf. 46(2), 87–137 (2009)CrossRefzbMATHGoogle Scholar
  13. 13.
    Milner, R.: Communicating and Mobile Systems: the π-Calculus. CUP (1999)Google Scholar
  14. 14.
    Rosa-Velardo, F., de Frutos-Escrig, D.: Forward analysis for petri nets with name creation. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 185–205. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  15. 15.
    Rosa-Velardo, F., Martos-Salgado, M.: Multiset rewriting for the verification of depth-bounded processes with name binding. Inf. Comput. 215, 68–87 (2012)CrossRefzbMATHMathSciNetGoogle Scholar
  16. 16.
    Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. CUP (2001)Google Scholar
  17. 17.
    Soare, R.I.: Recursively enumerable sets and degrees. Springer (1980)Google Scholar
  18. 18.
    Wies, T., Zufferey, D., Henzinger, T.A.: Forward analysis of depth-bounded processes. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 94–108. Springer, Heidelberg (2010)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Reiner Hüchting
    • 1
  • Rupak Majumdar
    • 2
  • Roland Meyer
    • 1
  1. 1.University of KaiserslauternGermany
  2. 2.MPI-SWSGermany

Personalised recommendations