Abstract
We investigate equivalence notions for concurrent systems. We consider “linear time” approaches where the system behaviour is characterised as the set of possible runs as well as “branching time” approaches where the conflict structure of systems is taken into account. We show that the usual interleaving equivalences, and also the equivalences based on steps (multisets of concurrently executed actions) are not preserved by refinement of actions. We prove that “linear time” partial order semantics, where causality in runs is explicit, is invariant under refinement. Finally, we consider various bisimulation equivalences based on partial orders and show that the strongest one of them is preserved by refinement whereas the others are not.
Notes This is an extended and updated version of our paper [GG a]. The extension consists of considering equivalences and refinement for the domain of flow event structures — instead of the subdomain of prime event structures — and allowing also infinite refinements and refinements with conflicts. This more general refinement operation was introduced in [GG b], however equivalences were not considered there. The results of this paper are also contained in [van Glabbeek b]. The work presented here has partly been carried out within the Esprit Basic Research Action 3148 (DEMON) and the Sonderforschungsbereich 342 of the TU München.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
L. Aceto, R. De Nicola, A. Fantechi: Testing Equivalences for Event Structures, Mathematical Models for the Semantics of Parallelism, LNCS 280, Springer-Verlag, 1987
L. Aceto, M. Hennessy: Towards Action-Refinement in Process Algebras, Proc. LICS'89, IEEE Computer Society Press, Washington, pp 138–145, 1989
D. Austry, G. Boudol: Algébre de processus et synchronisations, Theoretical Computer Science, Vol. 30, No. 1, pp 91–131, 1984
J.A. Bergstra, J.V. Tucker: Top-down Design and the Algebra of Communicating Processes, Science of Computer Programming, Vol. 5, No. 2, pp 171–199, 1985
E. Best, R. Devillers, A. Kiehn, L. Pomello: Fully Concurrent Bisimulation, Technical Report LIT 202, Université Libre de Bruxelles, Laboratoire d'Informatique Theorique, 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: On the Semantics of Concurrency: Partial Orders and Transition Systems, Proc. TAPSOFT 87, Vol. I, LNCS 249, Springer-Verlag, pp 123–137, 1987
G. Boudol, I. Castellani: Permutation of Transitions: An Event Structure Semantics for CCS and SCCS, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, Springer-Verlag, pp 411–427, 1989
W. Brauer, R. Gold, W. Vogler: Behaviour and Equivalence Preserving Refinements of Petri Nets, Report, Institut für Informatik, Technische Universität München, 1990
S.D. Brookes, C.A.R. Hoare, A.W. Roscoe: A Theory of Communicating Sequential Processes, Journal of the ACM, Vol. 31, No. 3, pp 560–599, 1984
L. Castellano, G. De Michelis, L. Pomello: Concurrency vs Interleaving: An Instructive Example, Bulletin of the EATCS 31, pp 12–15, 1987
P. Darondeau, P. Degano: Causal Trees, Proc. ICALP 89, LNCS 372, Springer-Verlag, pp 234–248, 1989
Ph. Darondeau, P. Degano: Event structures, Causal trees, and Refinements, to appear in Proc. MFCS 90, LNCS, Springer-Verlag, 1990
P. Degano, R. De Nicola, U. Montanari: Observational Equivalences for Concurrency Models, Formal Description of Programming Concepts — III, Proc. of the third IFIP WG 2.2 working conference, Elsevier Science Publishers B.V. (North Holland), pp 105–129, 1987
P. Degano, R. De Nicola, U. Montanari: A Distributed Operational Semantics for CCS Based on Condition/Event Systems, Acta Informatica, Vol. 26, No. 1/2, pp 59–91, 1988
P. Degano, R. De Nicola, U. Montanari: Partial Ordering Descriptions of Nondeterministic Concurrent Processes, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, Springer-Verlag, pp 438–466, 1989
R. De Nicola, M. Hennessy: Testing Equivalences for Processes, Theoretical Computer Science, Vol. 34, pp 83–133, 1984
R. Devillers: Maximality Preserving Bisimulation, Technical Report LIT 214, Université Libre de Bruxelles, Laboratoire d' Informatique Theorique, 1990
R.J. van Glabbeek: The Refinement Theorem for ST-Bisimulation Semantics, Report CS-R9002, Centrum voor Wiskunde en Informatica, Amsterdam 1990; to appear in: Proceedings IFIP Working Conference on Programming Concepts and Methods, Israel at sea Gallilee 1990
R.J. van Glabbeek: Comparative Concurrency Semantics and Refinement of Actions, Ph. D. Thesis, Free University, Amsterdam 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, U. Goltz: Refinement of Actions in Causality Based Models, Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, LNCS 430, Springer-Verlag, pp 267–300, 1990
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 CS-R8922, 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, pp 197–201, 1989
R. Gorrieri, S. Marchetti, U. Montanari: A 2 CCS: A Simple Extension of CCS for Handling Atomic Actions, Proc. CAAP'88, LNCS 299, Springer-Verlag, pp 258–270, 1988
M. Hennessy, R. Milner: Algebraic Laws for Nondeterminism and Concurrency, Journal of the ACM, Vol. 32, No. 1, pp 137–161, 1985
G.J. Milne: CIRCAL and the Representation of Communication, Concurrency and Time, Transactions on Programming languages and Systems (ACM), Vol. 7, No. 2, pp 270–298, 1985
R. Milner: A Calculus of Communicating Systems, LNCS 92, Springer-Verlag, 1980
R. Milner: Calculi for Synchrony and Asynchrony, Theoretical Computer Science, Vol. 25, No. 3, pp 267–310, 1983
M. Nielsen, U. Engberg, K.S. Larsen: Fully Abstract Models for a Process Language with Refinement, 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
D. Park: Concurrency and Automata on Infinite Sequences, Proc. 5th GI-Conference on Theoretical Computer Science, LNCS 104, Springer-Verlag, pp 167–183, 1981
C.A. Petri: Non-Sequential Processes, Interner Bericht 77-05, GMD, Institut für Informationssystemforschung, 1977
L. Pomello: Some Equivalence Notions for Concurrent Systems. An Overview, in: Advances in Petri Nets 1985, LNCS 222, Springer-Verlag, pp 381–400, 1986
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
D.A. Taubner, W. Vogler: The Step Failure Semantics, Proc. STACS 87, LNCS 247, Springer-Verlag, pp 348–359, 1987
B.A. Trakhtenbrot, A. Rabinovich, J. Hirshfeld: Nets of Processes, Technical Report 97/88, Tel Aviv Univ., 1988, see also: A Rabinovich, B.A. Trakhtenbrot: Behavior Structures and Nets, Fundamenta Informaticae, Vol. XI, No. 4, pp 357–404, 1988
F. Vaandrager: An Explicit Representation of Equivalence Classes of the History Preserving Bisimulation, Manuscript, CWI Amsterdam, 1989
W. Vogler: Failure Semantics Based on Interval Semiwords is a Congruence for Refinement, Proc. STACS'90, LNCS 415, Springer-Verlag, pp 285–297, 1990
W. Vogler: Bisimulation and Action Refinement, SFB-Bericht Nr. 342/10/90 A, Institut für Informatik, Technische Universität München, 1990
G. Winskel: Event Structures, 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
About this paper
Cite this paper
van Glabbeek, R.J., Goltz, U. (1990). Equivalences and refinement. In: Guessarian, I. (eds) Semantics of Systems of Concurrent Processes. LITP 1990. Lecture Notes in Computer Science, vol 469. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53479-2_13
Download citation
DOI: https://doi.org/10.1007/3-540-53479-2_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53479-2
Online ISBN: 978-3-540-46897-4
eBook Packages: Springer Book Archive