Linking Theories of Concurrency

  • He Jifeng
  • C. A. R. Hoare
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


We construct a Galois connection between the theories that underlie CCS [7] and CSP [4]. It projects the complete transition system for CCS onto exactly the subset that satisfies the healthiness conditions of CSP. The construction applies to several varieties of both calculi: CCS with strong, weak or barbed simulation, and CSP with trace refinement or failures refinement, or failures/divergence. We suggest the challenge of linking other theories of concurrency by Galois connection.


Transition System Binary Relation Complete Lattice Operational Semantic Transition Rule 
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.
    Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoretical Computer Sciences 37(1), 77–121 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the ACM 31 (1984)Google Scholar
  3. 3.
    Gardiner, P.: Power simulation and its relation to Traces and Failures Refinement. Theoretical Computer Science 309(1), 157–176 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Hoare, C.A.R.: Communicating sequential processes. Prentice Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  5. 5.
    Hoare, C.A.R., Jifeng, H.: Unifying theories of programming. Prentice Hall, Englewood Cliffs (1998)Google Scholar
  6. 6.
    Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and control 94(1) (1991)Google Scholar
  7. 7.
    Milner, R.: Communication and concurrency. Prentice Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  8. 8.
    Milner, R.: Communicating and mobile systems: the π -calculus. Cambridge University Press, Cambridge (1999)Google Scholar
  9. 9.
    Milner, R., Sangiorgi, D.: Barbed simulation. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 685–695. Springer, Heidelberg (1992)Google Scholar
  10. 10.
    De Nicola, R., Hennessy, M.: Testing equivalence for processes. Theoretical Computer Science 34 (1983)Google Scholar
  11. 11.
    Park, D.M.R.: Concurrency and automata on infinite sequences. In: Loeckx, J. (ed.) ICALP 1980. LNCS, vol. 14. Springer, Heidelberg (1980)Google Scholar
  12. 12.
    Plotkin, G.D.: A structural approach to operational semantics. Report DAIMI-FN-19, Computer Science Department, Arhus University, Denmark (1981)Google Scholar
  13. 13.
    Roscoe, A.W.: The theory and practice of concurrency. Prentice Hall, Englewood Cliffs (1998)Google Scholar
  14. 14.
    Tarski, A.: A lattice-theoretical fixedpoint theorem and its applications. Pacific Journal of Mathematics, Vil 5, 285–309 (1955)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • He Jifeng
    • 1
  • C. A. R. Hoare
    • 2
  1. 1.International Institute for Software TechnologyThe United Nations UniversityMacau
  2. 2.Microsoft ResearchCambridgeUK

Personalised recommendations