On the Complexity of Termination Inference for Processes

  • Romain Demangeon
  • Daniel Hirschkoff
  • Naoki Kobayashi
  • Davide Sangiorgi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4912)


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.


Polynomial Time Partial Order Type System Simple Type Termination Inference 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    The Terminator Project: proof tools for termination and liveness (2007),
  2. 2.
    Cook, B., Podelski, A., Rybalchenko, A.: Proving Thread Termination. In: Proc. of PLDI 2007, pp. 320–330. ACM Press, New York (2007)CrossRefGoogle Scholar
  3. 3.
    Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good, pp. 265–276 (2007)Google Scholar
  4. 4.
    Deng, Y., Sangiorgi, D.: Ensuring Termination by Typability. Information and Computation 204(7), 1045–1082 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    Igarashi, A., Kobayashi, N.: Type Reconstruction for Linear Pi-Calculus with I/O Subtyping. Information and Computation 161(1), 1–44 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Kobayashi, N.: TyPiCal: Type-based static analyzer for the Pi-Calculus (2007),
  9. 9.
    Kobayashi, N., Sangiorgi, D.: From Deadlock-Freedom and Termination to Lock-Freedom (submitted 2007)Google Scholar
  10. 10.
    Rehof, J., Mogensen, T.: Tractable Constraints in Finite Semilattices. Science of Computer Programming 35(2), 191–221 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Sangiorgi, D.: Termination of Processes. Mathematical Structures in Computer Science 16(1), 1–39 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    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)Google Scholar
  13. 13.
    Yoshida, N., Berger, M., Honda, K.: Strong Normalisation in the Pi-Calculus. Information and Computation 191(2), 145–202 (2004)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Romain Demangeon
    • 1
  • Daniel Hirschkoff
    • 1
  • Naoki Kobayashi
    • 2
  • Davide Sangiorgi
    • 3
  1. 1.ENS Lyon, CNRS, INRIA, UCBL, UMR 5668France
  2. 2.Tohoku UniversityJapan
  3. 3.Università di BolognaItaly

Personalised recommendations