An asynchronous model of locality, failure, and process mobility

  • Roberto M. Amadio
Regular Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1282)


We present a model of distributed computation which is based on a fragment of the π-calculus relying on asynchronous communication. We enrich the model with the following features: the explicit distribution of processes to locations, the failure of locations and their detection, and the mobility of processes. Our contributions are two folds. At the specification level, we give a synthetic and flexible formalization of the features mentioned above. At the verification level, we provide original methods to reason about the bisimilarity of processes in the presence of failures.


π-calculus Bisimulation Asynchronous communication Locations Models of distributed systems Failures and failures detection Mobility of processes 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Amadio. An asynchronous model of locality, failure, and process mobility. RR-INRIA 3109. Available at Scholar
  2. 2.
    R. Amadio, I. Castellani, and D. Sangiorgi. On bisimulations for the asynchronous π-calculus. In CONCUR 96, SLNCS. 1119, 1996.Google Scholar
  3. 3.
    R. Amadio, L. Leth, and B. Thomsen. From a concurrent λ-calculus to the π-calculus. In Proc. Foundations of Computation Theory 95, SLNCS 965, 1995.Google Scholar
  4. 4.
    R. Amadio and S. Prasad. Localities and Failures (Extended Summary). In Proc. of FST-TCS94 SLNCS 880, 1994.Google Scholar
  5. 5.
    M. Boreale. On the expressiveness of internal mobility in name passing calculi. In CONCUR 96, SNLCS 1119, 1996.Google Scholar
  6. 6.
    G. Boudol. Asynchrony and the π-calculus. RR-INRIA 1702, 1992.Google Scholar
  7. 7.
    G. Boudol. Some chemical abstract machines. In Proc. of REX School, SLNCS 803, 1993.Google Scholar
  8. 8.
    T. Chandra and S. Toueg. Unreliable failure detectors for reliable distributed systems. Journal of ACM, 43(2):225–267, 1996.CrossRefGoogle Scholar
  9. 9.
    C. Fournet and G. Gonthier. The reflexive CRAM and the join-calculus. Proc. POPL, 1996.Google Scholar
  10. 10.
    C. Fournet, G. Gonthier, J.-J. Levy, L. Maranget, and D. Rémy. A calculus of mobile agents. In CONCUR 96, SLNCS 1119, 1996.Google Scholar
  11. 11.
    K. Honda and M. Tokoro. An object calculus for asynchronous communication. Proc. ECOOP 91, Geneve, 1991.Google Scholar
  12. 12.
    N. Kobayashi, B. Pierce, and D. Turner. Linearity in the π-calculus. Proc. POPL, 1996.Google Scholar
  13. 13.
    R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Process, Parts 1–2. Information and Computation, 100(1):1–77, 1992.CrossRefGoogle Scholar
  14. 14.
    B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. In Proc. LICS, 1993.Google Scholar
  15. 15.
    D. Sangiorgi. π-calculus, internal mobility and agent-passing calculi. In Proc Tapsoft 95, SLNCS 915, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Roberto M. Amadio
    • 1
  1. 1.Université de Provence (LIM)Marseille

Personalised recommendations