Skip to main content
SpringerLink
Log in
Book cover

Annual Symposium on Theoretical Aspects of Computer Science

STACS 1994: STACS 94 pp 569–580Cite as

Transition system specifications in stalk format with bisimulation as a congruence

  • Conference paper
  • First Online:

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

Abstract

A many-sorted variant, called stalk format, of the single sorted tyft-format for transition system specifications, introduced by Groote and Vaandrager, is proposed. The stalk format is shown to be a convenient formalism to express continuation-style transition systems for which the existing formats seem less adequate. Extending a similar result for the single sorted case, it holds that for an appropriate generalization of strong bisimilarity for the present many-sorted setting, bisimulation with respect to a transition system specification in stalk format, is a congruence. The present format is compared with several existing ones in the literature, viz. De Simone-, GSOS- and pure tyft-format.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. America and J.W. de Bakker. Designing equivalent models for process creation. Theoretical Computer Science, 60:109–176, 1988.

    Google Scholar 

  2. P.H.M. America and J.J.M.M. Rutten. A parallel object-oriented language: Design and semantic foundations. In J.W. de Bakker, editor, Languages for Parallel Architectures: Design, Semantics, Implementation Models, pages 1–49. Wiley, 1989.

    Google Scholar 

  3. J.W. de Bakker. Comparative semantics for flow of control in logic programming without logic. Information and Computation, 91:123–179, 1991.

    Google Scholar 

  4. R. Bol and J.F. Groote. The meaning of negative premises in transition system specifications. In J. Leach Albert, B. Monien, and M. Rodríguez Artalejo, editors, Proc. ICALP'91, pages 481–494. LNCS 510, 1991.

    Google Scholar 

  5. B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can't be traced. In Proc. Principles of Programming Languages, pages 229–239. San Diego, 1988.

    Google Scholar 

  6. J.W. de Bakker and J.N. Kok. Uniform abstraction, atomicity and contractions in the comparative semantics of Concurrent Prolog. In Proc. of the International Conference on Fifth Generation Computer Systems, pages 347–355. Institute for New Generation Computer Technology, 1988.

    Google Scholar 

  7. J.A. Bergstra, J.W. Klop, and E.-R. Olderog. Readies and failures in the algebra of communicating processes. SIAM Journal on Computing, 17:1134–1177, 1988.

    Google Scholar 

  8. J.W. de Bakker and E.P. de Vink. CCS for OO and LP. In S. Abramsky and T.S.E. Maibaum, editors, Proc. TAPSOFT'91, volume 2, pages 1–28. LNCS 494, 1991.

    Google Scholar 

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

    Google Scholar 

  10. J.W. de Bakker and E.P. de Vink. Bisimulation semantics for concurrency with atomicity and action refinement. Technical Report CS-R9210, CWI, 1992.

    Google Scholar 

  11. J.C.M. Baeten and C. Verhoef. A congruence theorem for structured operational semantics with predicates. In E. Best, editor, Proc. CON-CUR'93, pages 477–492. LNCS 715, 1993.

    Google Scholar 

  12. A. EliËns and E.P. de Vink. Asynchronous rendez-vous in Distributed Logic Programming. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Semantics: Foundations and Applications, pages 174–203. LNCS 666, 1993.

    Google Scholar 

  13. W.J. Fokkink. The tyft/tyxt format reduces to tree rules. Technical report, CWI, 1993. Draft. Extended abstract to appear in proc. Theoretical Aspects of Computer Science'94.

    Google Scholar 

  14. J.F. Groote. Transition system specifications with negative premises. In J.C.M. Baeten and J.W. Klop, editors, Proc. CONCUR'90, Theories of Concurrency: Unification and Extension, pages 332–342. LNCS 458, 1990.

    Google Scholar 

  15. J.F. Groote and F.W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100:202–260, 1992.

    Google Scholar 

  16. K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. In Proc. Principles of Programming Languages, pages 344–352, 1989.

    Google Scholar 

  17. V. van Oostrom and E.P. de Vink. Transition system specifications in stalk format with bisimulation as a congruence. Technical Report IR-332, Vrije Universiteit, 1993. Obtainable through anonymous ftp from ftp.cs.vu.nl as /pub/oostrom/stalk.ps.Z.

    Google Scholar 

  18. J.J.M.M. Rutten. Deriving denotational models for bisimulation from Structured Operational Semantics. In M. Broy and C.B. Jones, editors, Programming concepts and methods, proc. of the IFIP Working Group 2.2/2.3 Working Conference, pages 155–177. North-Holland, 1990.

    Google Scholar 

  19. J.J.M.M. Rutten. Processes as terms: non-well-founded models for bisimulation. Mathematical Structures in Computer Science, 2:257–275, 1992.

    Google Scholar 

  20. R. de Simone. Calculabilité et Expressivité dans l'Algèbre de Processus Parallèles MEIJE. PhD thesis, Thèse de 3eme cycle, Université de Paris VII, 1984.

    Google Scholar 

  21. C. Verhoef. A congruence theorem for structured operational semantics with predicates and negative premises. Report CSN-93/18, Eindhoven University of Technology, Eindhoven, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, Vrije Universiteit, De Boelelaan 1081a, NL-1081 HV, Amsterdam

    V. van Oostrom & E. P. de Vink

Authors
  1. V. van Oostrom
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. E. P. de Vink
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Patrice Enjalbert Ernst W. Mayr Klaus W. Wagner

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

van Oostrom, V., de Vink, E.P. (1994). Transition system specifications in stalk format with bisimulation as a congruence. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds) STACS 94. STACS 1994. Lecture Notes in Computer Science, vol 775. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57785-8_172

Download citation

  • DOI: https://doi.org/10.1007/3-540-57785-8_172

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57785-0

  • Online ISBN: 978-3-540-48332-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation