Normal Bisimulations in Calculi with Passivation

  • Sergueï Lenglet
  • Alan Schmitt
  • Jean-Bernard Stefani
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5504)


Behavioral theory for higher-order process calculi is less well developed than for first-order ones such as the π-calculus. In particular, effective coinductive characterizations of barbed congruence, such as the notion of normal bisimulation developed by Sangiorgi for the higher-order π-calculus, are difficult to obtain. In this paper, we study bisimulations in two simple higher-order calculi with a passivation operator, that allows the interruption and thunkification of a running process. We develop a normal bisimulation that characterizes barbed congruence, in the strong and weak cases, for the first calculus which has no name restriction operator. We then show that this result does not hold in the calculus extended with name restriction.


Behavioral Theory Behavioral Equivalence Closed Process Evaluation Context Process Calculus 
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.


  1. 1.
    Cao, Z.: More on bisimulations for higher order π-calculus. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 63–78. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, p. 140. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  3. 3.
    Castagna, G., Vitek, J., Zappa Nardelli, F.: The Seal Calculus. Information and Computation 201(1) (2005)Google Scholar
  4. 4.
    Godskesen, J.C., Hildebrandt, T.: Extending howe’s method to early bisimulations for typed mobile embedded resources with local names. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 140–151. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Hildebrandt, T., Godskesen, J.C., Bundgaard, M.: Bisimulation congruences for Homer — a calculus of higher order mobile embedded resources. Technical Report ITU-TR-2004-52, IT University of Copenhagen (2004)Google Scholar
  6. 6.
    Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Information and Computation 124(2) (1996)Google Scholar
  7. 7.
    Lanese, I., Pérez, J.A., Sangiorgi, D., Schmitt, A.: On the expressiveness and decidability of higher-order process calculi. In: 23rd Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, Los Alamitos (2008)Google Scholar
  8. 8.
    Lenglet, S., Schmitt, A., Stefani, J.B.: Normal bisimulations in process calculi with passivation. Technical Report RR 6664, INRIA (2008),
  9. 9.
    Merro, M., Zappa Nardelli, F.: Behavioral theory for mobile ambients. Journal of the ACM 52(6) (2005)Google Scholar
  10. 10.
    Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, Department of Computer Science, University of Edinburgh (1992)Google Scholar
  11. 11.
    Sangiorgi, D.: Bisimulation for higher-order process calculi. Information and Computation 131(2) (1996)Google Scholar
  12. 12.
    Sangiorgi, D., Walker, D.: The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  13. 13.
    Schmitt, A., Stefani, J.B.: The Kell Calculus: A Family of Higher-Order Distributed Process Calculi. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 146–178. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  14. 14.
    Thomsen, B.: Plain chocs: A second generation calculus for higher order processes. Acta Informatica 30(1) (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Sergueï Lenglet
    • 1
  • Alan Schmitt
    • 2
  • Jean-Bernard Stefani
    • 2
  1. 1.Université Joseph FourierGrenobleFrance
  2. 2.INRIA Grenoble-Rhône-AlpesFrance

Personalised recommendations