Abstract
We investigate the class $procBD$ of π-Calculus processes that are bounded in the function depth. First, we show that boundedness in depth has an intuitive characterisation when we understand processes as graphs: a process is bounded in depth if and only if the length of the simple paths is bounded. The proof is based on a new normal form for the π-Calculus called anchored fragments. Using this concept, we then show that processes of bounded depth have well-structured transition systems (WSTS). As a consequence, the termination problem is decidable for this class of processes. The instantiation of the WSTS framework employs a new well-quasi-ordering for processes in $procBD$.
Chapter PDF
Similar content being viewed by others
References
P. A. Abdulla, K. Ćerans, B. Jonsson, and Y.-K. Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160(1–2):109–127, 2000.
R. M. Amadio and C. Meyssonnier. On decidability of the control reachability problit in the asynchronous $π$-calculus. Nordic Journal of Computing, 9(1):70–101, 2002.
L. Caires. Behavioural and spatial observations in a logic for the πCalculus. In FOSSACS 2004, volume 2987 of LNCS, pages 72–89. Springer-Verlag, 2004.
M. Dam. Model checking mobile processes. Information and Computation, 129(1):35–51, 1996.
Y. Deng and D. Sangiorgi. Ensuring termination by typability. Information and Computation, 204(7):1045–1082, 2006.
J. Engelfriet and T. Gelsita. Multisets and structural congruence of the pi-calculus with replication. Theoretical Computer Science, 211(1–2):311–337, 1999.
J. Engelfriet and T. Gelsita. Structural inclusion in the pi-calculus with replication. Theoretical Computer Science, 258(1–2):131–168, 2001.
J. Engelfriet and T. Gelsita. A new natural structural congruence in the pi-calculus with replication. Acta Informatica, 40(6):385–430, 2004.
G.-L. Ferrari, S. Gnesi, U. Montanari, and M. Pistore. A model-checking verification environment for mobile processes. ACM Transactions on Software Engineering and Methodology, 12(4):440–473, 2003.
A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89(2):144–179, 1990.
A. Finkel and Ph. Schnoebelen. Well-structured transition systits everywhere! Theoretical Computer Science, 256(1–2):63–92, 2001.
A. Habel. Hyperedge Replacitent: Grammars and Languages, volume 643 of LNCS. Springer-Verlag, 1992.
G. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3), 2(7):326–336, 1952.
R. Meyer. A theory of structural stationarity in the π-calculus. Under revision, 2008.
G. Milne and R. Milner. Concurrent processes and their syntax. JACM, 26(2):302–321, 1979.
R. Milner. Flowgraphs and flow algebras. JACM, 26(4):794–818, 1979.
R. Milner. Communicating and Mobile Systits: the π-Calculus. Cambridge University Press, 1999.
D. Sangiorgi and D. Walker. The π-calculus: a Theory of Mobile Processes. Cambridge University Press, 2001.
N. Yoshida, M. Berger, and K. Honda. Strong normalisation in the πcalculus. Information and Computation, 191(2):145–202, 2004.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Meyer, R. (2008). On Boundedness in Depth in the π-Calculus. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds) Fifth Ifip International Conference On Theoretical Computer Science – Tcs 2008. IFIP International Federation for Information Processing, vol 273. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-09680-3_32
Download citation
DOI: https://doi.org/10.1007/978-0-387-09680-3_32
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-09679-7
Online ISBN: 978-0-387-09680-3
eBook Packages: Computer ScienceComputer Science (R0)