Testing equivalences for processes

  • R. de Nicola
  • M. C. B. Hennessy
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)


Given a set of processes and a set of tests on these processes we show how to define in a natural way three different equivalences on processes. These equivalences are applied to a particular language CCS. We give associated complete proof systems and fully abstract models. These models have a simple representation in terms of trees.


Semantic Theory Operational Semantic Proof System Successful State Denotational Semantic 
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]
    Darondeau,Ph. An enlarged definition and complete axiomatization of observational congruence of finite processes, LNCS 137, pp. 47–62, 1982.Google Scholar
  2. [2]
    De Nicola,R. and Hennessy,M. Testing equivalences for processes, Technical Report CSR-123-82, University of Edinburgh.Google Scholar
  3. [3]
    Goguen,J.A., Thatcher,J.W., Wright,J.B. Initial algebra semantics and continuous algebras, JACM Vol. 24, No. 1, pp. 68–95, 1977.Google Scholar
  4. [4]
    Guessarian,I. Algebraic semantics, LNCS 99, 1981.Google Scholar
  5. [5]
    Hennessy,M. Powerdomains and nondeterministic recursive definitions, LNCS 137, pp. 178–193, 1982.Google Scholar
  6. [6]
    Hennessy,M., Plotkin,G. A term model for CCS, LNCS 88, pp. 261–274, 1980.Google Scholar
  7. [7]
    Hennessy,M., Milner,R. On observing nondeterminism and concurrency, LNCS 85, pp. 299–309, 1980.Google Scholar
  8. [8]
    Hoare,C.A.R. A model for communicating sequential processes, Technical Monograph Prg-22, Computing Laboratory, University of Oxford, 1981.Google Scholar
  9. [9]
    Hoare,C.A.R., Brookes,S.D. and Roscoe,A.D. A theory of communicating sequential sequential processes, Technical Monograph Prg-16, Computing Laboratory, University of Oxford, 1981.Google Scholar
  10. [10]
    Kennaway,J.K. and Hoare,C.A.R. A theory of nondeterminism, LNCS 85, pp. 338–350, 1980.Google Scholar
  11. [11]
    Kennaway,J.K. Formal semantics of nondeterminism and parallelism, Ph.D. thesis, University of Oxford, 1981.Google Scholar
  12. [12]
    Milner, R. A calculus of communicating systems, LNCS 92, 1980.Google Scholar
  13. [13]
    Plotkin,G. A powerdomain construction, SIAM J. on Computing, No. 5, pp. 452–486, 1976.Google Scholar
  14. [14]
    Rounds,W.C., and Brookes,S.D. Possible futures, acceptances, refusals and communicating processes, Proc. of 22nd FOCS Annual Symposium, Nashville Tennessee, October 1981.Google Scholar
  15. [15]
    Scott, D.S. Data types as lattices, SIAM J. on Computing, Vol. 5, No. 3, 1976.Google Scholar
  16. [16]
    Smyth,M.B. Power domains, JCSS, Vol. 2, pp. 23–36, 1978.Google Scholar
  17. [17]
    Stoy,J. Denotational semantics: the Scott-Strachey approach to programming language theory, MIT Press, 1977.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • R. de Nicola
    • 1
  • M. C. B. Hennessy
    • 1
  1. 1.Dept. of Computer ScienceUniversity of EdinburghEdinburghScotland

Personalised recommendations