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)
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
L. Aceto and M. Hennessy. Towards action-refinement in process algebras. Information and Computation, 103: 204–269, 1993.
M. A. Bednarczyk. Categories of Asynchronous Systems. PhD thesis, University of Sussex, Oct. 1987.
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.
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.
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.
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.
W. R. Cleaveland, editor. Concur 992, volume 630 of Lecture Notes in Computer Science. Springer-Verlag, 1992.
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.
P. Darondeau and P. Degano. Refinement of actions in event structures and causal trees. Theoretical Comput. Sci., 118: 21–48, 1993.
P. Degano, R. De Nicola, and U. Montanari. A partial ordering semantics for CCS. Theoretical Comput Sci75: 223–262, 1991.
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.
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.
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.
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.
J. F. Groote. Transition system specifications with negative premises. Theoretical Comput Sci., 118: 263–299, 1993.
L. Jategaonkar and A. Meyer. Testing equivalences for Petri nets with action refinement. In Cleaveland [8], pages 17–31.
R. Langerak. Transformations and Semantics for LOTOS. PhD thesis, University of Twente, Nov. 1992.
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.
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.
A. Rensink. Posets for configurations! In Cleaveland [8], pages 269–285.
A. Rensink. Models and Methods for Action Refinement. PhD thesis, University of Twente, Enschede, Netherlands, Aug. 1993.
A. Rensink. Order isomorphism does not preserve independence. Bull. Eur. Ass. Theoret. Comput. Sci., 51: 228–235, Oct. 1993.
M. W. Shields. Concurrent machines. The Computer Journal, 28 (5): 449–465, 1985.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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