Abstract
We consider an operator for refinement of actions to be used in the design of concurrent systems. Actions on a given level of abstraction are replaced by more complicated processes on a lower level. This is done in such a way that the behaviour of the refined system may be inferred compositionally from the behaviour of the original system and from the behaviour of the processes substituted for actions. We define this refinement operation for causality based models like event structures and Petri nets. For Petri nets, we relate it to other approaches for refining transitions.
Contributed in part to Esprit Basic Research Action 3148 (DEMON).
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
L. Aceto, M. Hennessy: Towards Action-Refinement in Process Algebras, in: Proc. LICS'89, Asilomar, California, IEEE Computer Society Press, Washington, pp 138–145, 1989
J.A. Bergstra, J.V. Tucker: Top-down Design and the Algebra of Communicating Processes, Science of Computer Programming 5, pp 171–199, 1985
E. Best, R. Devillers, A. Kiehn, L. Pomello: Fully Concurrent Bisimulation, unpublished, 1989
G. Boudol: Atomic Actions (Note), Bulletin of the EATCS 38, pp 136–144, 1989
G. Boudol: Computations of Distributed Systems, Part 1: Flow Event structures and Flow Nets, report INRIA Sophia Antipolis, to appear
G. Boudol, I. Castellani: Permutation of Transitions: An Event Structure Semantics for CCS and SCCS, in: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, Springer-Verlag, pp 411–427, 1989
L. Castellano, G. De Michelis, L. Pomello: Concurrency vs Interleaving: An Instructive Example, Bulletin of the EATCS 31, pp 12–15, 1987
J. Desel, A. Merceron: Vicinity Respecting Net Morphisms, in: Advances in Petri Nets 89, LNCS, Springer-Verlag, to appear
H.J. Genrich, E. Stankiewicy-Wiechno: A Dictionary of some Basic Notions of Net Theory, in: Net Theory and Applications, LNCS 84, Springer-Verlag, pp 519–535, 1979
J.L. Gischer: The Equational Theory of Pomsets, Theoretical Computer Science 61, pp 199–224, 1988
R.J. van Glabbeek: The Refinement Theorem for ST-Bisimulation Semantics, Report, Centrum voor Wiskunde en Informatica, Amsterdam 1990; to appear in: Proceedings IFIP Working Conference Programming Concepts and Methodes, Israel at sea Gallilee 1990
R.J. van Glabbeek, U. Goltz: Equivalence Notions for Concurrent Systems and Refinement of Actions, Arbeitspapiere der GMD 366, February 1989, Extended Abstract in Proc. MFCS 89, LNCS 379, Springer-Verlag, pp 237–248, 1989
R.J. van Glabbeek, F.W. Vaandrager: Petri Net Models for Algebraic Theories of Concurrency, Proc. PARLE, Vol. II, LNCS 259, Springer-Verlag, pp 224–242, 1987
R.J. van Glabbeek, W.P. Weijland: Refinement in Branching Time Semantics, Report CSR8922, Centrum voor Wiskunde en Informatica, Amsterdam 1989; in: J.W. de Bakker, 25 jaar semantiek, liber amicorum, Centrum voor Wiskunde en Informatica, Amsterdam 1989, pp 247–252; and in: Proceedings AMAST Conference, Iowa City, USA, 1989, pp 197–201
R. Gorrieri, S. Marchetti, U. Montanari: A 2 CCS: A Simple Extension of CCS for Handling Atomic Actions in: Proc. CAAP'88, LNCS 299, Springer-Verlag, 1988
E.P. Gribomont: Stepwise Refinement and Concurrency: A Small Exercise, in: Mathematics of Program Construction, LNCS 375, Springer-Verlag, pp 219–238, 1989
W. Korczyński: An Algebraic Characterization of Concurrent Systems, Fundamenta Informaticae, Vol.11, No. 2, pp 171–194, 1988
R. Milner: A Calculus of Communicating Systems, LNCS 92, Springer-Verlag, 1980
J. Meseger, U. Montanari: Petri Nets are Monoids, in: Proc. LICS '88, Edinburgh, 1988
M. Nielsen, U. Engberg, K.S. Larsen: Fully Abstract Models for a Process Language with Refinement, in Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, Springer-Verlag, pp 523–548, 1989
M. Nielsen, G.D. Plotkin, G. Winskel: Petri Nets, Event Structures and Domains, Part I, Theoretical Computer Science, Vol. 13, No. 1, pp 85–108, 1981
C.A. Petri: Non-Sequential Processes, Interner Bericht 77-05, GMD, Institut für Informationssystemforschung, 1977
V.R. Pratt: Modelling Concurrency with Partial Orders, International Journal of Parallel Programming, Vol. 15, No. 1, pp 33–71, 1986
W. Reisig: Petri Nets, EATCS Monographs on Theoretical Computer Science 4, Springer-Verlag, 1985
W. Reisig: Petri Nets in Software Engineering, in: Petri Nets: Applications and Relationships to other Models of Concurrency, LNCS 255, Springer-Verlag, pp 63–96, 1987
I. Suzuki, T. Murata: A Method for Stepwise Refinement and Abstraction of Petri Nets, Journal of Computer and System Sciences, Vol. 27, No. 1, pp 51–76, 1983
R. Valette: Analysis of Petri Nets by Stepwise Refinements, Journal of Computer and System Sciences, Vol. 18, pp 35–46, 1979
W. Vogler: Behaviour Preserving Refinements of Petri Nets, in: Proc. 12th Int. Workshop on Graph Theoretic Concepts in Computer Science, LNCS 246, Springer-Verlag, pp 82–93, 1987
W. Vogler: Failure Semantics Based on Interval Semiwords is a Congruence for Refinement, in Proc. STACS'90, LNCS, Springer-Verlag, to appear
G. Winskel: Event Structures, in: Petri Nets: Applications and Relationships to Other Models of Concurrency, LNCS 255, Springer-Verlag, pp 325–392, 1987
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Glabbeek, R., Goltz, U. (1990). Refinement of actions in causality based models. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness. REX 1989. Lecture Notes in Computer Science, vol 430. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52559-9_68
Download citation
DOI: https://doi.org/10.1007/3-540-52559-9_68
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52559-2
Online ISBN: 978-3-540-47035-9
eBook Packages: Springer Book Archive