Abstract
Depth-bounded processes form the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. In this paper we develop an adequate domain of limits for the well-structured transition systems that are induced by depth-bounded processes. An immediate consequence of our result is that there exists a forward algorithm that decides the covering problem for this class. Unlike backward algorithms, the forward algorithm terminates even if the depth of the process is not known a priori. More importantly, our result suggests a whole spectrum of forward algorithms that enable the effective verification of a large class of mobile systems.
Chapter PDF
Similar content being viewed by others
References
Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313–321 (1996)
Amadio, R.M., Meyssonnier, C.: On decidability of the control reachability problem in the asynchronous pi-calculus. Nord. J. Comput. 9(1), 70–101 (2002)
Bauer, J., Wilhelm, R.: Static analysis of dynamic communication systems by partner abstraction. In: SAS, pp. 249–264 (2007)
Busi, N., Gabbrielli, M., Zavattaro, G.: Replication vs. recursive definitions in channel based calculi. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 133–144. Springer, Heidelberg (2003)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Löding, C., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (2008), http://tata.gforge.inria.fr/ (release November 18, 2008)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977)
Dam, M.: Model checking mobile processes. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 22–36. Springer, Heidelberg (1993)
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. Comput. 89(2), 144–179 (1990)
Finkel, A., Goubault-Larrecq, J.: Forward Analysis for WSTS, Part I: Completions. In: STACS. Dagstuhl Sem. Proc., vol. 09001, 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. LNCS, vol. 5556, pp. 188–199. Springer, Heidelberg (2009)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63–92 (2001)
Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, Enlarge and Check: New algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72(1), 180–203 (2006)
Janssens, D., Lens, M., Rozenberg, G.: Computation graphs for actor grammars. J. Comput. Syst. Sci. 46(1), 60–90 (1993)
Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)
Laver, R.: On Fraïssé’s Order Type Conjecture. Ann. of Math. 93(1), 89–111 (1971)
Lipton, R.J.: The reachability problem requires exponential space. Technical Report 62, Yale University (1976)
Meyer, R.: On boundedness in depth in the pi-calculus. In: IFIP TCS. IFIP, vol. 273, pp. 477–489. Springer, Heidelberg (2008)
Meyer, R., Gorrieri, R.: On the relationship between pi-calculus and finite place/transition petri nets. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 463–480. Springer, Heidelberg (2009)
Milner, R.: Flowgraphs and flow algebras. J. ACM 26(4), 794–818 (1979)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, I. Inf. Comput. 100(1), 1–40 (1992)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, II. Inf. Comput. 100(1), 41–77 (1992)
Nash-Williams, C.S.J.A.: On better-quasi-ordering transfinite sequences. Proc. Camb. Phil. Soc. 64, 273–290 (1968)
Nešetřil, J., de Mendez, P.O.: Tree-depth, subgraph coloring and homomorphism bounds. Eur. J. Comb. 27(6), 1022–1041 (2006)
Ostrovský, K.: On Modelling and Analysing Concurrent Systems. PhD thesis, Chalmers University of Technology and Gotebörg University (2005)
Sangiorgi, D.: pi-calculus, internal mobility, and agent-passing calculi. Theor. Comput. Sci. 167(1&2), 235–274 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wies, T., Zufferey, D., Henzinger, T.A. (2010). Forward Analysis of Depth-Bounded Processes. In: Ong, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2010. Lecture Notes in Computer Science, vol 6014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12032-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-12032-9_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12031-2
Online ISBN: 978-3-642-12032-9
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science