Skip to main content
SpringerLink
Log in

An Event-Based SOS for a Language with Refinement

  • Conference paper
Structures in Concurrency Theory

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

The notion of action refinement has been studied intensively in the past few years. It is usually introduced in the form of an operator in a process algebraic language, for which a denotational semantics in a suitable model is then given. In this paper we complement this approach by defining a corresponding operational semantics for refinement, in the form of derivation rules for a transition relation. Because of the (well-known) fact that ordinary transition systems are not expressive enough to capture the effects of refinement, we use an event-based transition system model described elsewhere in the literature. The operational semantics of refinement thus defined is equivalent (in fact event isomorphic) to the usual denotational semantics.

Based on [22, Chapter 3]. This work was initiated while the author was staying at the University of Twente, and is partially supported by the Esprit BRA Project 3096 SPEC (Formal Methods and Tools for the Development of Distributed and Real Time Systems) and the Esprit Working Group 6067 CALIBAN (Casual Calculi Based on Nets)

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Aceto and M. Hennessy. Adding action refinement to a finite process algebra. In J. Leach Albert, B. Monien, and M. R. Artalejo, editors, Automata, Languages and Programming, volume 510 of Lecture Notes in Computer Science, pages 506–519. Springer-Verlag, 1991. To apear in Information and Computation.

    Google Scholar 

  2. L. Aceto and M. Hennessy. Towards action-refinement in process algebras. Information and Computation, 103: 204–269, 1993.

    Article  MathSciNet  MATH  Google Scholar 

  3. M. A. Bednarczyk. Categories of Asynchronous Systems. PhD thesis, University of Sussex, Oct. 1987.

    Google Scholar 

  4. E. Best, R. Devillers, and J. Esparza. General refinement and recursion operators for the Petri box calculus. In P. Enjalbert, A. Finkel, and K. W. Wagner, editors, STACS 93, volume 665 of Lecture Notes in Computer Science, pages 130–140. Springer-Verlag, 1993.

    Google Scholar 

  5. G. Boudol and I. Castellani. Permutations of transitions: An event structure semantics for CCS and SCCS. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 411–427. Springer-Verlag, 1989.

    Google Scholar 

  6. G. Boudol and I. Castellani. Flow models of distributed computations: Three equivalent semantics for CCS. Rapports de Recherche 1484, INRIA, July 1991. To appear in Information and Computation.

    Google Scholar 

  7. N. Busi, R. van Glabbeek, and R. Gorrieri. Axiomatising ST bisimulation equivalence. In E.-R. Olderog, editor, Programming Concepts, Methods and Calculi, volume A-56 of IFIP Transactions, pages 169–188. IFIP, 1994.

    Google Scholar 

  8. W. R. Cleaveland, editor. Concur 992, volume 630 of Lecture Notes in Computer Science. Springer-Verlag, 1992.

    Google Scholar 

  9. I. Czaja, R. J. van Glabbeek, and U. Goltz. Interleaving semantics and action refinement with atomic choice. In G. Rozenberg, editor, Advances in Petri Nets 1992, volume 609 of Lecture Notes in Computer Science, pages 89–109. Springer-Verlag, 1992.

    Google Scholar 

  10. P. Darondeau and P. Degano. Refinement of actions in event structures and causal trees. Theoretical Comput. Sci., 118: 21–48, 1993.

    Article  MathSciNet  MATH  Google Scholar 

  11. P. Degano, R. De Nicola, and U. Montanari. A partial ordering semantics for CCS. Theoretical Comput Sci75: 223–262, 1991.

    Google Scholar 

  12. P. Degano and R. Gorrieri. An operational definition of action refinement. Technical Report TR-28/92, Università di Pisa, 1992. To appear in Information and Computation.

    Google Scholar 

  13. R. van Glabbeek and U. Goltz. Equivalence notions for concurrent systems and refinement of actions. In A. Kreczmar and G. Mirkowska, editors, Mathematical Foundations of Computer Science 1989, volume 379 of Lecture Notes in Computer Science, pages 237–248. Springer-Verlag, 1989.

    Google Scholar 

  14. R. van Glabbeek and U. Goltz. Refinement of actions in causality based models. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems — Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 267–300. Springer-Verlag, 1990.

    Google Scholar 

  15. U. Goltz, R. Gorrieri, and A. Rensink. On syntactic and semantic action refinement. In M. Hagiya and J. C. Mitchell, editors, Theoretical Aspects of Computer Software, volume 789 of Lecture Notes in Computer Science, pages 385–404. Springer-Verlag, Apr. 1994.

    Google Scholar 

  16. J. F. Groote. Transition system specifications with negative premises. Theoretical Comput Sci., 118: 263–299, 1993.

    Article  MathSciNet  MATH  Google Scholar 

  17. L. Jategaonkar and A. Meyer. Testing equivalences for Petri nets with action refinement. In Cleaveland [8], pages 17–31.

    Google Scholar 

  18. R. Langerak. Transformations and Semantics for LOTOS. PhD thesis, University of Twente, Nov. 1992.

    Google Scholar 

  19. M. Nielsen, V. Sassone, and G. Winskel. Relationships between models for concurrency. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, A Decade of Concurrency, volume 803 of Lecture Notes in Computer Science, pages 425–476. Springer-Verlag, 1994.

    Google Scholar 

  20. G. M. Pinna and A. Poigne. On the nature of events. In Mathematical Foundations of Computer Science 1992, Lecture Notes in Computer Science. Springer-Verlag, 1992.

    Google Scholar 

  21. A. Rensink. Posets for configurations! In Cleaveland [8], pages 269–285.

    Google Scholar 

  22. A. Rensink. Models and Methods for Action Refinement. PhD thesis, University of Twente, Enschede, Netherlands, Aug. 1993.

    Google Scholar 

  23. A. Rensink. Order isomorphism does not preserve independence. Bull. Eur. Ass. Theoret. Comput. Sci., 51: 228–235, Oct. 1993.

    MATH  Google Scholar 

  24. M. W. Shields. Concurrent machines. The Computer Journal, 28 (5): 449–465, 1985.

    Article  MathSciNet  MATH  Google Scholar 

  25. E. W. Stark. Connections between a concrete and an abstract model of concurrent systems. In M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Mathematical Foundations of Programming Semantics, volume 442 of Lecture Notes in Computer Science, pages 53–79. Springer-Verlag, 1990.

    Google Scholar 

  26. W. Vogler. Failures semantics based on interval semi words is a congruence for refinement. In C. Choffrut and T. Lengauer, editors, STACS 90, volume 415 of Lecture Notes in Computer Science, pages 285–297. Springer-Verlag, 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, University of Hildesheim, Hildesheim, Germany

    Arend Rensink

Authors
  1. Arend Rensink
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, Humboldt-Universität zu Berlin, Unter den Linden 6, D-10099, Berlin, Germany

    Jörg Desel Dr. rer. nat.

Rights and permissions

Reprints and permissions

Copyright information

© 1995 British Computer Society

About this paper

Cite this paper

Rensink, A. (1995). An Event-Based SOS for a Language with Refinement. In: Desel, J. (eds) Structures in Concurrency Theory. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3078-9_20

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3078-9_20

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19982-3

  • Online ISBN: 978-1-4471-3078-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation