Abstract
We study type systems for termination in the π-calculus from the point of view of type inference. We analyse four systems by Deng and Sangiorgi. We show that inference can be done in polynomial time for two of these, but that this is not the case for the two most expressive systems. To remedy this, we study two modifications of these type systems that allow us to recover a polynomial type inference.
This work has been supported by the french ANR project “ARASSIA — Modularité Dynamique Fiable”, by the EC project “SENSORIA” and Italian MIUR Project n. 2005015785 ”Logical Foundations of Distributed Systems and Mobile Code”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
The Terminator Project: proof tools for termination and liveness (2007), http://research.microsoft.com/terminator/
Cook, B., Podelski, A., Rybalchenko, A.: Proving Thread Termination. In: Proc. of PLDI 2007, pp. 320–330. ACM Press, New York (2007)
Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good, pp. 265–276 (2007)
Deng, Y., Sangiorgi, D.: Ensuring Termination by Typability. Information and Computation 204(7), 1045–1082 (2006)
Fournet, C., Laneve, C., Maranget, L., Rémy, D.: Implicit Typing à la ML for the Join-Calculus. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 196–212. Springer, Heidelberg (1997)
Gay, S.J.: A Sort Inference Algorithm for the Polyadic Pi-Calculus. In: Proc. of POPL 1993, pp. 429–438. ACM Press, New York (1993)
Igarashi, A., Kobayashi, N.: Type Reconstruction for Linear Pi-Calculus with I/O Subtyping. Information and Computation 161(1), 1–44 (2000)
Kobayashi, N.: TyPiCal: Type-based static analyzer for the Pi-Calculus (2007), http://www.kb.ecei.tohoku.ac.jp/~koba/typical/
Kobayashi, N., Sangiorgi, D.: From Deadlock-Freedom and Termination to Lock-Freedom (submitted 2007)
Rehof, J., Mogensen, T.: Tractable Constraints in Finite Semilattices. Science of Computer Programming 35(2), 191–221 (1999)
Sangiorgi, D.: Termination of Processes. Mathematical Structures in Computer Science 16(1), 1–39 (2006)
Vasconcelos, V.T., Honda, K.: Principal Typing Schemes in a Polyadic pi-Calculus. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 524–538. Springer, Heidelberg (1993)
Yoshida, N., Berger, M., Honda, K.: Strong Normalisation in the Pi-Calculus. Information and Computation 191(2), 145–202 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Demangeon, R., Hirschkoff, D., Kobayashi, N., Sangiorgi, D. (2008). On the Complexity of Termination Inference for Processes. In: Barthe, G., Fournet, C. (eds) Trustworthy Global Computing. TGC 2007. Lecture Notes in Computer Science, vol 4912. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78663-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-78663-4_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78662-7
Online ISBN: 978-3-540-78663-4
eBook Packages: Computer ScienceComputer Science (R0)