Skip to main content
SpringerLink
Log in

The linear time — Branching time spectrum II

The semantics of sequential systems with silent moves extended abstract

  • Conference paper
  • First Online:
CONCUR'93 (CONCUR 1993)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 715))

Included in the following conference series:

Abstract

This paper studies semantic equivalences and preorders for sequential systems with silent moves, restricting attention to the ones that abstract from successful termination, stochastic and real-time aspects of the investigated systems, and the structure of the visible actions systems can perform. It provides a parameterized definition of such a preorder, such that most such preorders and equivalences found in the literature are obtained by a suitable instantiation of the parameters. Other instantiations yield preorders that combine properties from various semantics. Moreover, the approach shows several ways in which preorders that were originally only considered for systems without silent moves, most notably the ready simulation, can be generalized to an abstract setting, and how preorders that were originally only considered for for systems without divergence, such as the coupled simulation, can be extended to divergent systems. All preorders come with—or rather as—a modal characterization, and when possible also a relational characterization. The paper concludes with some pros and cons of the preorders.

This work was supported by ONR under grant number N00014-92-J-1974.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.C.M. Baeten (1986): Procesalgebra. Programmatuurkunde. Kluwer, Deventer. In Dutch.

    Google Scholar 

  2. J.C.M. Baeten, J.A. Bergstra & J.W. Klop (1987): On the consistency of Koomen's fair abstraction rule. Theoretical Computer Science 51(1/2), pp. 129–176.

    Article  Google Scholar 

  3. J.C.M. Baeten & R.J. van Glabbeek (1987): Another look at abstraction in process algebra. In Th. Ottmann, editor: Proceedings 14th ICALP, Karlsruhe, Lecture Notes in Computer Science 267, Springer-Verlag, pp. 84–94.

    Google Scholar 

  4. J. van Benthem, J. van Eijck & V. Stebletsova (1993): Modal logic, transition systems and processes. Report CS-R9321, CWI, Amsterdam.

    Google Scholar 

  5. J.A. Bergstra, J.W. Klop & E.-R. Olderog (1987): Failures without chaos: a new process semantics for fair abstraction. In M. Wirsing, editor: Formal Description of Programming Concepts — III, Proceedings of the 3thIFIP WG 2.2 working conference, Ebberup 1986, North-Holland, Amsterdam, pp. 77–103.

    Google Scholar 

  6. S.D. Brookes & A.W. Roscoe (1985): An improved failures model for communicating processes. In S.D. Brookes, A.W. Roscoe & G. Winskel, editors: Seminar on Concurrency, Lecture Notes in Computer Science 197, Springer-Verlag, pp. 281–305.

    Google Scholar 

  7. M.C. Browne, E.M. Clarke & O. Grümberg (1988): Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science 59(1, 2), pp. 115–131.

    Article  Google Scholar 

  8. F. Cherief (1992): Contributions à la sémantique du parallélisme: bisimulations pour le raffinement et le vrai parallélisme. PhD thesis, Univ. Grenoble.

    Google Scholar 

  9. R. De Nicola & F.W. Vaandrager (1990): Three logics for branching bisimulation (extended abstract). In Proceedings 5th Annual Symposium on Logic in Computer Science, Philadelphia, USA, IEEE Computer Society Press, pp. 118–129. Full version available as Rapporto di Ricerca SI-92/07, Dipartimento di Scienze dell'Informazione, Università degli Studi di Roma “La Sapienza”, November 1992.

    Google Scholar 

  10. R.J. van Glabbeek (1990): The linear time — branching time spectrum. In J.C.M. Baeten & J.W. Klop, editors: Proceedings CONCUR 90, Amsterdam, Lecture Notes in Computer-Science 458, Springer-Verlag, pp. 278–297.

    Google Scholar 

  11. R.J. van Glabbeek & F.W. Vaandrager (1989): Modular specifications in process algebra — with curious queues (extended abstract). In M. Wirsing & J.A. Bergstra, editors: Algebraic Methods: Theory, Tools and Applications, Workshop Passau 1987, Lecture Notes in Computer Science 394, Springer-Verlag, pp. 465–506.

    Google Scholar 

  12. R.J. van Glabbeek & W.P. Weijland (1990): Branching time and abstraction in bisimulation semantics. Technical Report TUM-I9052, SFB-Bericht Nr. 342/29/90 A, Institut für Informatik, Technische Universität München, Munich, Germany. Extended abstract in G.X. Ritter, editor: Information Processing 89, Proceedings of the IFIP 11th World Computer Congress, San Fransisco, USA 1989, Elsevier Science Publishers B.V. (North-Holland), 1989, pp. 613–618.

    Google Scholar 

  13. J.F. Groote & F.W. Vaandrager (1992): Structured operational semantics and bisimulation as a congruence. Information and Computation 100(2), pp. 202–260.

    Article  Google Scholar 

  14. M. Hennessy & G.D. Plotkin (1980): A term model for CCS. In P.Dembiński, editor: 9th Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 88, Springer-Verlag, pp. 261–274.

    Google Scholar 

  15. L. Lamport (1977): Proving the correctness of multiprocess programs. IEEE Trans. Software Engin. 3, pp. 125–143.

    Google Scholar 

  16. R. Langerak (1989): A testing theory for LOTOS using deadlock detection. In E. Brinksma, G. Scollo & C.A. Vissers, editors: Proceedings 9th IFIP WG6.1 International Symposium on Protocol Specification, Testing, and Verification, Enschede, The Netherlands.

    Google Scholar 

  17. R. Milner (1981): A modal characterisation of observable machine-behaviour. In G. Astesiano & C. Bohm, editors: Proceedings CAAP 81, Lecture Notes in Computer Science 112, Springer-Verlag, pp. 25–34.

    Google Scholar 

  18. R. Milner (1985): Lectures on a calculus for communicating systems. In S.D. Brookes, A.W. Roscoe & G. Winskel, editors: Seminar on Concurrency, Lecture Notes in Computer Science 197, Springer-Verlag, pp. 197–220.

    Google Scholar 

  19. R. Milner (1990): Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor: Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201–1242. Alternatively see Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989, of which an earlier version appeared as A Calculus of Communicating Systems, LNCS 92, Springer-Verlag, 1980.

    Google Scholar 

  20. J. Parrow & P. Sjödin (1992): Multiway synchronization verified with coupled simulation. In W.R. Cleaveland, editor: Proceedings CONCUR 92, Stony Brook, NY, USA, Lecture Notes in Computer Science 630, Springer-Verlag, pp. 518–533.

    Google Scholar 

  21. A.W. Roscoe (1988): Unbounded nondeterminism in CSP. In To papers on CSP, Technical Monograph PRG-67, Programming Research Group, Oxford University Computing Laboratory, Oxford, England, pp. 27–80.

    Google Scholar 

  22. C. Stirling (1987): Modal logics for communicating systems. Theoretical Computer Science 49, pp. 311–347.

    Google Scholar 

  23. I. Ulidowski (1992): Equivalences on observable processes. In Proceedings 7thAnnual Symposium on Logic in Computer Science, Santa Cruz, California, IEEE Computer Society Press, pp. 148–159.

    Google Scholar 

  24. D.J. Walker (1990): Bisimulation and divergence. Information and Computation 85(2), pp. 202–241.

    Article  Google Scholar 

  25. W.P. Weijland (1989): Synchrony and asynchrony in process algebra. PhD thesis, University of Amsterdam.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Stanford University, 94305, Stanford, CA, USA

    R. J. van Glabbeek

Authors
  1. R. J. van Glabbeek
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Eike Best

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

van Glabbeek, R.J. (1993). The linear time — Branching time spectrum II. In: Best, E. (eds) CONCUR'93. CONCUR 1993. Lecture Notes in Computer Science, vol 715. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57208-2_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-57208-2_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57208-4

  • Online ISBN: 978-3-540-47968-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation