Nothing Special   »   [go: up one dir, main page]

Skip to main content
Log in

Extensional equivalences for transition systems

  • Published:
Acta Informatica Aims and scope Submit manuscript

Summary

Various notions of systems equivalence based on the reactions of systems to stimuli from the outside world are presented and compared. These notions have been proposed in the literature to allow abstraction from unwanted details in models of concurrent and communicating systems. The equivalences, already defined for different theories of concurrency, will be compared by adapting their definitions to labelled transition systems, a model which underlies many others. In the presentation of each equivalence, the aspects of system behaviours which are ignored and the identifications which are forced will be stressed. It will be shown that many equivalences, although defined very differently by following different intuitions about systems behaviour, turn out to be the same or to differ only in minor detail for a large class of transition systems.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Similar content being viewed by others

References

  1. Brookes, S.D., Hoare, C.A.R., Roscoe, A.D.: A Theory of Communicating Sequential Processes. J. ACM 31, 560–599 (1984)

    Google Scholar 

  2. Brookes, S.D., Rounds, W.C.: Behavioural Equivalence Relations induced by Programming Logics. Proc. ICALP 83, Lect. Notes Comput. Sci. Vol. 154, pp. 97–108. Berlin, Heidelberg, New York: Springer 1983

    Google Scholar 

  3. Brookes, S.D.: On the Relationship between CCS and CSP. Proc. ICALP '83, Lect. Notes Comput. Sci. Vol. 154, pp. 83–96. Berlin, Heidelberg, New York: Springer 1983

    Google Scholar 

  4. Darondeau, P.: An Enlarged Definition and Complete Axiomatization of Observational Congruence of Finite Processes. Lect. Notes Comput. Sci. Vol. 137, pp. 47–62. Berlin, Heidelberg, New York: Springer 1982

    Google Scholar 

  5. De Nicola, R., Hennessy, M.: Testing Equivalences for Processes. Theor. Comput. Sci. 34, 83–133 (1984)

    Google Scholar 

  6. Ginzburg, S.: Algebraic Theory of Automata. New York: Academic Press 1968

    Google Scholar 

  7. Hennessy, M., Milner, R.: Algebraic Laws for Nondeterminism and Concurrency. J. ACM, 32, 137–161 (1985)

    Google Scholar 

  8. Hoare, C.A.R.: Communicating Sequential Processes. Commun. ACM 21, 666–677 (1978)

    Google Scholar 

  9. Hoare, C.A.R.: A Model for Communicating Sequential Processes. Technical Monograph Prg-22, Computing Laboratory, University of Oxford 1981

  10. Keller, R.: Formal Verification of Parallel Programs. Commun. ACM 19, 561–572 (1976)

    Google Scholar 

  11. Kennaway, J.K.: Formal Semantics of Nondeterminism and Parallelism. Ph.D. Thesis, University of Oxford 1981

  12. Kennaway, J.K., Hoare, C.A.R.: A Theory of Nondeterminism. Lect. Notes Comput. Sci. Vol.85, pp. 338–350. Berlin, Heidelberg, New York: Springer 1980

    Google Scholar 

  13. Milner, R.: A Calculus of Communicating Systems. Lect. Notes Comput. Sci. Vol. 92, Berlin, Heidelberg, New York 1980

  14. Milner, R.: Calculi for Synchrony and Asynchrony. Theor. Comput. Sci. 25, 267–310 (1983)

    Google Scholar 

  15. Milner, R.: A Complete Inference System for a Class of Regular Behaviours. J. Comput. Syst. Sci. 28, 439–466 (1984)

    Google Scholar 

  16. Moore, E.: Gedanken Experiments on Sequential Machines. In: Automata Studies (Shannon, C.E., McCarthy, J., eds.) Princeton: University Press 1956

    Google Scholar 

  17. Olderog, E.R., Hoare, C.A.R.: Specification-Oriented Semantics for Communicating Processes, Proc. ICALP 83. Lect. Notes Comput. Sci. Vol. 154, pp. 561–572, Berlin, Heidelberg, New York: Springer 1983

    Google Scholar 

  18. Park, D.: Concurrency and Automata an Infinite Sequences. Proc. 5th GI Conference. Lect. Notes Comput. Sci. Vol. 104, pp. 167–183. Berlin, Heidelberg, New York: Springer 1981

    Google Scholar 

  19. Plotkin, G.: A Powerdomain Construction, SIAM J. Comput. 5, 452–486 (1976)

    Google Scholar 

  20. Plotkin, G.: A Structural Approach to Operational Semantics. Lect. Notes, Aarhus University, Aarhus 1981

    Google Scholar 

  21. Sanderson, M.T.: Proof Techniques for CCS. Ph.D. Thesis, University of Edinburgh, CST-19-82, 1982

  22. Smyth, M.B.: Power Domains. J. Comput. Syst. Sci. 2, 23–36 (1978)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Rights and permissions

Reprints and permissions

About this article

Cite this article

De Nicola, R. Extensional equivalences for transition systems. Acta Informatica 24, 211–237 (1987). https://doi.org/10.1007/BF00264365

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00264365

Keywords

Navigation