Abstract
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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
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)
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)
Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: LICS, pp. 70–80 (June 1998)
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)
Finkel, A.: Reduction and covering of infinite reachability trees. Inf. Comp. 89(2), 144–179 (1990)
Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part I: Completions. In: STACS, pp. 433–444 (2009)
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)
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)
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)
Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)
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)
Meyer, R.: A theory of structural stationarity in the π-calculus. Acta Inf. 46(2), 87–137 (2009)
Milner, R.: Communicating and Mobile Systems: the π-Calculus. CUP (1999)
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)
Rosa-Velardo, F., Martos-Salgado, M.: Multiset rewriting for the verification of depth-bounded processes with name binding. Inf. Comput. 215, 68–87 (2012)
Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. CUP (2001)
Soare, R.I.: Recursively enumerable sets and degrees. Springer (1980)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hüchting, R., Majumdar, R., Meyer, R. (2014). Bounds on Mobility. In: Baldan, P., Gorla, D. (eds) CONCUR 2014 – Concurrency Theory. CONCUR 2014. Lecture Notes in Computer Science, vol 8704. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44584-6_25
Download citation
DOI: https://doi.org/10.1007/978-3-662-44584-6_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44583-9
Online ISBN: 978-3-662-44584-6
eBook Packages: Computer ScienceComputer Science (R0)