Correctness and full abstraction of metric semantics for concurrency

  • J. J. M. M. Rutten
Technical Contributions
Part of the Lecture Notes in Computer Science book series (LNCS, volume 354)


Four different semantic models are given for a simple uniform programming language, containing constructs for parallel composition, global nondeterminism and communication: linear semantics, failure semantics, readiness semantics, and branching semantics. The mathematical framework used consists of complete metric spaces. All models and operators are given as fixed points of suitably defined contractions. This allows for a uniform presentation and an easy comparison of these models. It is shown that the latter three semantics all are correct and that the failure semantics is fully abstract with respect to the linear semantics. Although these results are not new, we believe the uniformity of the way they are presented here to be of some interest.

Key words and phrases

concurrency complete metric spaces contractions operational semantics denotational semantics compositionality correctness full abstraction 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

8. References

  1. [AP86]
    K. Apt, G. Plotkin, Countable nondeterminism and random assignment, Journal of the Association for Computing Machinery, Vol. 33, No. 4, 1986, pp. 724–767.Google Scholar
  2. [AR88]
    P. America, J.J.M.M. Rutten, Solving reflexive domain equations in a category of complete metric spaces, in: Proceedings of the Third Workshop on Mathematical Foundations of Programming Language Semantics (M. Main, A. Melton, M. Mislove, D. Schmidt, Eds.), Lecture Notes in Computer Science 298, Springer-Verlag, 1988, pp. 254–288. (To appear in the Journal of Computer and System Sciences.)Google Scholar
  3. [BHR84]
    S. Brookes, C. Hoare, W. Roscoe, A theory of communicating sequential processes, J. Assoc. Comput. Mach. 31, No. 3, 1984, pp. 560–599.MathSciNetGoogle Scholar
  4. [BK87]
    J.A. Bergstra, J.W. Klop, A convergence theorem in process algebra, Report CS-R8733, Centre for Mathematics and Computer Science, Amsterdam, 1987.Google Scholar
  5. [BKO87]
    J.A. Bergstra, J.W. Klop, E.-R. Olderog, Readies and failures in the algebra of communicating processes (revised version), Report CS-R8748, Centre for Mathematics and Computer Science, Amsterdam, 1987. (To appear in: SIAM Journal of Computing, 1988.)Google Scholar
  6. [BM88]
    J.W. de Bakker, J.-J. Ch. Meyer, Metric semantics for concurrency, Report CS-R8803, Centre for Mathematics and Computer Science, Amsterdam, 1988.Google Scholar
  7. [BKMOZ86]
    J.W. de Bakker, J.N. Kok, J.-J. Ch. Meyer, E.-R. Olderog, J.I. Zucker, Contrasting themes in the semantics of imperative concurrency, in: Current Trends in Concurrency (J.W. de Bakker, W.P. de Roever, G. Rozenberg, Eds.), Lecture Notes in Computer Science 224, Springer-Verlag, 1986, pp. 51–121.Google Scholar
  8. [BMOZ88]
    J.W. de Bakker, J.-J. Ch. Meyer, E.-R. Olderog, J.I. Zucker, Transition systems, metric spaces and ready sets in the semantics of uniform concurrency, Journal of Computer and System Sciences Vol 36 (number 2), 1988, pp. 158–224.CrossRefGoogle Scholar
  9. [BZ82]
    J.W. de Bakker, J.I. Zucker, Processes and the denotational semantics of concurrency, Information and Control 54 (1982), pp. 70–120.CrossRefGoogle Scholar
  10. [De85]
    R. De Nicola, Testing equivalences and fully abstract models for communicating processes, Ph.D. Thesis, report CST-36-85, Department of Computer Science, University of Edinburgh, 1985.Google Scholar
  11. [Du66]
    J. Dugundji, Topology, Allen and Bacon, Rockleigh, N.J., 1966.Google Scholar
  12. [En77]
    E. Engelking, General topology, Polish Scientific Publishers, 1977.Google Scholar
  13. [HP79]
    M. Hennessy, G.D. Plotkin, Full abstraction for a simple parallel programming language, in: Proceedings 8th MFCS (J. Bečvář ed.), Lecture Notes in Computer Science 74, Springer-Verlag, 1979, pp. 108–120.Google Scholar
  14. [Ho85]
    C.A.R. Hoare, Communicating sequential processes, Prentice Hall International, 1985.Google Scholar
  15. [KR88]
    J.N. Kok, J.J.M.M. Rutten, Contractions in comparing concurrency semantics, in: Proceedings 15th ICALP, Tampere, 1988, Lecture Notes in Computer Science 317, Springer-Verlag, 1988, pp. 317–332.Google Scholar
  16. [Mic51]
    E. Michael, Topologies on spaces of subsets, in: Trans. AMS 71 (1951), pp. 152–182.Google Scholar
  17. [Mil80]
    R. Milner, A Calculus of communicating systems, Lecture Notes in Computer Science 92, Springer-Verlag, 1980.Google Scholar
  18. [Mu85]
    K. Mulmuley, Full abstraction and semantic equivalence, Ph.D. Thesis, report CMU-CS-85-148, Computer Science Department, Carnegie-Mellon, 1985.Google Scholar
  19. [OH86]
    E.-R. Olderog, C.A.R. Hoare, Specification-oriented semantics for communicating processes, Acta Informaticae 23, 1986, pp. 9–66.Google Scholar
  20. [Pl76]
    G.D. Plotkin, A powerdomain construction, SIAM J. Comp. 5 (1976), pp. 452–487.CrossRefGoogle Scholar
  21. [Pl81]
    G.D. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Comp. Sci. Dept., Aarhus Univ. 1981.Google Scholar
  22. [Pl83]
    G.D. Plotkin, An operational semantics for CSP, in: Formal Description of Programming Concepts II (D. Bjørner ed.) North-Holland, Amsterdam (1983), pp. 199–223.Google Scholar
  23. [St86]
    A. Stoughton, Fully abstract models of programming languages, Ph.D. Thesis, report CST-40-86, Department of Computer Science, University of Edinburgh, 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • J. J. M. M. Rutten
    • 1
  1. 1.Centre for Mathematics and Computer ScienceAmsterdamThe Netherlands

Personalised recommendations