Skip to main content
SpringerLink
Log in

A congruence theorem for structured operational semantics with predicates

  • 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

We proposed a syntactical format, the path format, for structured operational semantics in which predicates may occur. We proved that strong bisimulation is a congruence for all the operators that can be defined within the path format. To show that this format is useful we provided many examples that we took from the literature about CCS, CSP, and ACP; they do satisfy the path format but no formats proposed by others. The examples include concepts like termination, convergence, divergence, weak bisimulation, a zero object, side conditions, functions, real time, discrete time, sequencing, negative premises, negative conclusions, and priorities (or a combination of these notions).

Partial support received from the European Communities under CONCUR 2, BRA 7166.

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. L. Aceto, M. Hennessy, Termination, deadlock and divergence, JACM 39(1):147–187, 1992.

    Article  Google Scholar 

  2. J. C. M. Baeten, J. A. Bergstra, Discrete Time Process Algebra, Report P9208b, Programming Research Group, University of Amsterdam, 1992.

    Google Scholar 

  3. J. C. M. Baeten, J. A. Bergstra, Process algebra with a zero object, in: J. C. M. Baeten and J. W. Klop, editors, Proceedings CONCUR 90, Amsterdam, LNCS 458, pp. 83–98, Springer-Verlag, 1990.

    Google Scholar 

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

    Article  Google Scholar 

  5. J. C. M. Baeten, J. A. Bergstra, J. W. Klop, Syntax and defining equations for an interrupt mechanism in process algebra, Fundamenta Informaticae IX, pp. 127–168, 1986.

    Google Scholar 

  6. J. C. M. Baeten, R. J. van Glabbeek, Merge and termination in process algebra, in: K. V. Nori, editor, Proceedings 7th Conference on Foundations of Software Technology and Theoretical Computer Science, Pune, India, LNCS 287, pp. 153–172, Springer-Verlag, 1987.

    Google Scholar 

  7. J. C. M. Baeten and F. W. Vaandrager, An algebra for process creation, Acta Informatica 29, pp. 303–334, 1992.

    Article  Google Scholar 

  8. J. C. M. Baeten, W. P. Weijland, Process algebra, Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, 1990.

    Google Scholar 

  9. J. A. Bergstra, J. W. Klop, Algebra of communicating processes with abstraction, TCS 37, 77–121, 1985.

    Article  Google Scholar 

  10. J. A. Bergstra, J. W. Klop, Fixed point semantics in process algebras, MC report IW 206, Mathematical Centre, Amsterdam, 1982. Revised version: J. A. Bergstra, J. W. Klop, A convergence theorem in process algebra, in Ten years of concurrency semantics: selected papers of the Amsterdam Concurrency Group, editors J. W. de Bakker, J. J. M. M. Rutten, World Scientific, pp. 164–195, 1992.

    Google Scholar 

  11. B. Bloom, S. Istrail, and A. R. Meyer, Bisimulation can't be traced: preliminary report, In: Proceedings 15th ACM Symposium on Principles of Programming Languages, San Diego, California, pp. 229–239, 1988.

    Google Scholar 

  12. W. J. Fokkink, personal communication, January 1993.

    Google Scholar 

  13. K. Futatsugi, J.A. Goguen, J.-P. Jouannaud, J. Meseguer, Principles of OBJ2, in Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, editor B. Reid, pp. 52–66, ACM, 1985.

    Google Scholar 

  14. R. J. van Glabbeek, Bounded nondeterminism and the approximation induction principle in process algebra, In: Proceedings STACS 87 (F. J. Brandenburg, G. Vidal-Naquet, M. Wirsing, eds.), LNCS 247, Springer Verlag, pp. 336–347, 1987.

    Google Scholar 

  15. J. F. Groote, Transition system specifications with negative premises, Report CS-R9850, CWI, Amsterdam, 1989. An extended abstract appeared in: see [3] pp. 332–341.

    Google Scholar 

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

    Article  Google Scholar 

  17. A. Ingólfsdóttir, B. Thomsen, Semantic Models for CCS with Values, in: Proceedings Chalmers Workshop on Concurrency, 1991, pp. 215–242, Report PMG-R63, Chalmers University of Technology and University of Göteborg, 1992.

    Google Scholar 

  18. A. S. Klusener, Completeness in real time process algebra, Technical Report CS-R9106, CWI, Amsterdam, 1991. An extended abstract appeared in J. C. M. Baeten and J. F. Groote, editors, Proceedings CONCUR 91, Amsterdam, LNCS 527, pp. 376–392, 1991.

    Google Scholar 

  19. C. P. J. Koymans and J. L. M. Vrancken, Extending process algebra with the empty process É›, Logic Group Preprint Series Nr. 1, CIF, Utrecht University, 1985.

    Google Scholar 

  20. R. Milner, A calculus of communicating systems, LNCS 92, Springer Verlag, 1980.

    Google Scholar 

  21. F. Moller and C. Tofts, A Temporal Calculus of Communicating Systems, in: see [3], pp. 401–4151990.

    Google Scholar 

  22. D. M. R. Park, Concurrency and automata on infinite sequences, In P. Duessen (ed.) 5th GI Conference, LNCS 104, pp. 167–183, Springer-Verlag, 1981.

    Google Scholar 

  23. G. D. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

    Google Scholar 

  24. S. Schneider, An Operational Semantics for Timed CSP, in: see [17] pp. 428–456. To appear in Information and Computation.

    Google Scholar 

  25. R. de Simone, Higher-level synchronising devices in Meije-SCCS, TCS 37, pp. 245–267, 1985.

    Google Scholar 

  26. Wang Yi, Towards a Theory of Testing for CCS with Probability, in: see [17] pp. 476–492.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computing Science, Eindhoven University of Technology, P.O. Box 513, 5600, MB Eindhoven, The Netherlands

    J. C. M. Baeten & C. Verhoef

Authors
  1. J. C. M. Baeten
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. C. Verhoef
    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

Baeten, J.C.M., Verhoef, C. (1993). A congruence theorem for structured operational semantics with predicates. 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_33

Download citation

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

  • 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