Comparative Concurrency Semantics
and Refinement of Actions
Academisch Proefschrift
ter verkrijging van de graad van doctor aan
de Vrije Universiteit te Amsterdam,
op woensdag 16 mei 1990 te 15.30 uur
door
Robert Jan van Glabbeek,
geboren te Eindhoven
Second edition
Centrum voor Wiskunde en Informatica
1996
Promotoren:
prof. dr. J.W. Klop
and
prof. dr. J.A.
Bergstra
Referent:
prof. dr. G. Winskel
Contents
Introduction 7
 The linear time  branching time spectrum 17
 Semantic equivalences on labelled transition systems 22
 The semantic lattice 38
 Complete axiomatizations 50
 Modular specifications in process algebra  with curious queues 55
 Module logic 61
 Process algebra 66
 Applications of the module approach in process algebra 80
 Queues 89
 A protocol verification 102
Appendix: Logics 111
 Branching time and abstraction in bisimulation semantics 117
 Branching and abstraction 120
 Axioms 130
 Branches and traces 143
 Completeness proofs 149
 Correspondence 158
 Refinement 159
 Divergence 163
 Modal characterizations 164
 Refinement of actions in causality based models 173
 Refinement of actions in prime event structures 181
 Refinement of actions in flow event structures 186
 Configuration structures and refinement of actions 193
 Refinement of transitions in Petri nets 197
 Partial order semantics for refinement of actions  neither necessary
nor always sufficient but appropriate when used with care  213
 Equivalence notions for concurrent systems and refinement of actions 223
 Interleaving semantics 225
 Step semantics 227
 `Linear time' partial order semantics 230
 `Branching time' partial order semantics 231
 The refinement theorem for STbisimulation semantics 243
 Concurrent systems and refinement of actions 247
 The behaviour of concurrent systems I 249
 Equivalence notions for concurrent systems I 250
 The behaviour of concurrent systems II 255
 Equivalence notions for concurrent systems II 257
 The refinement theorems 265
References 273
Affiliations
Most of the work reported in this thesis was done when I was employed
at the
Centre for Mathematics and Computer Science (CWI) in Amsterdam.
The manuscript was finalized during my employment at
the
Technical University of Munich, Postfach 202420, D8000 München
2. Chapter II is joint work with
Frits Vaandrager, and Chapter III with
Peter Weijland, both affiliated with the Centre for Mathematics and
Computer Science. Chapters IV, V and VI are joint work with Ursula
Goltz, Gesellschaft für Mathematik und Datenverarbeitung,
Postfach 1240, D5205 Sankt Augustin 1.
My current affiliation is:
Computer Science Department,
Stanford University, CA 943059045, USA.
Support
The work reported in this thesis has been supported by
ESPRIT project no. 432, An Integrated Formal Approach to
Industrial Software Development (METEOR) (Chapter II, III, V, VI),
RACE project no. 1046, Specification and Programming Environment
for Communication Software (SPECS) (Chapter II),
ESPRIT Basic Research Action 3006, Theories of Concurrency:
Unification and Extension (CONCUR) (Chapter III),
ESPRIT Basic Research Action 3148, Design Methods Based on Nets
(DEMON) (Introduction, Chapter I, III, IV and VI)
and Sonderforschungsbereich 342 of the TU München (Introduction,
Chapter I, III and VI). The work on this second edition has been
supported by ONR under grant number N0001492J1974.
Chapter I was partly written in the preparation of
a course Comparative Concurrency Semantics, given at the University of
Amsterdam, spring 1988.
Prior Publications
The material presented in the seven chapters of this thesis can also
be found in
[19,
7,
23,
16,
14,
20,
15]
respectively. Furthermore Chapter II without Sections 4 and 5
appeared in the Ph.D. Thesis of Frits Vaandrager
(Algebraic Techniques for Concurrency and their Application,
University of Amsterdam, CWI, Amsterdam 1989)
and the first two sections of Chapter III partly appeared in the
Ph.D. Thesis of Peter Weijland
(Synchrony and Asynchrony in Process Algebra,
University of Amsterdam, CWI, Amsterdam 1989).
Finally, Section 6 of Chapter III appeared as
[12].
Acknowledgements
Jan Willem Klop has been an ideal promotor for me. He was always ready
to discuss my work, but let me free to pursue my own goals in my own
way. It has been a great pleasure to have him as a supervisor.
I also like to express my gratitude to Jan Bergstra, not only for
being my second promotor, but also for initiating my employment at CWI
and organizing a very interesting scientific environment. Moreover
I appreciated the many discussions with him, in which he was always
full of ideas.
I benefited immensely from the collaboration with Frits Vaandrager.
It is in my opinion a rare privilege to discuss ones ideas at the time
they are being formed with someone able of grasping them in full and
providing feedback.
With Frits I could discuss all my work in depth and he contributed
numerous useful ideas.
I thank Ursula Goltz for our fruitful cooperation since 1987. Our joint
work on action refinement forms an important constituent of this thesis.
This work was initiated by a discussion with Albert Meyer and
ErnstRüdiger Olderog at ICALP 87 in Karlsruhe, to whom I also
express my gratitude.
I am grateful to my colleagues Jos Baeten and Jan Friso Groote for our
pleasant collaboration and for their useful comments on earlier versions
of parts of this thesis.
Furthermore I gratefully acknowledge the discussions and correspondence
with Alex Rabinovich, Walter Vogler, Wolfgang Reisig, Vaughan Pratt,
Tony Hoare, Ilaria Castellani, Rocco De Nicola, Pierpaolo Degano,
Ugo Montanari and Gérard Boudol that contributed to the work
reported in this thesis.
I thank the participants of the weekly Process Algebra Meetings (as far as not
mentioned already): Wiet Bouma, Jeroen Bruijning, Nicolien Drost,
Henk Goeman, Karst Koymans, Sjouke Mauw, Kees Middelburg,
Hans Mulder, Alban Ponse, Gerard Renardel de Lavalette, Piet Rodenburg,
Gert Veltink, Jos Vrancken, FerJan de Vries, Peter Weijland, Freek
Wiedijk and Han Zuidweg, for numerous lively discussions and comments.
More in general, my years at the
CWI Department of
Software Technology,
headed by Jaco de Bakker, will remain a pleasant memory for its
excellent working conditions and friendly atmosphere.
It is a pleasure to thank Glynn Winskel for his kind willingness
to referee this thesis and to take part in the examination committee.
Thanks are also due to the printing department of CWI for its fast
production of the original thesis, and especially to Jan Friso and Frits for
helping me with the drawings, headers, etc. during the last part of an
exciting race against the clock.
Finally, special thanks goes to Gertrud Jacobs for her careful
preparation of Chapters IV, V and VI of the original manuscript, and
for being available whenever she was needed.
1. Comparative concurrency semantics
This thesis is about comparative concurrency semantics.
Concurrency is the study of concurrent systems.
Often concurrency as area of scientific research is placed
in computer science. In that case the systems which are the subject
of study are taken to be computers or computer programs.
However, much theory in the field of concurrency applies
equally well to other systems, like machines, elementary particles,
protocols, networks of falling dominoes or human beings.
Concurrent or parallel systems  as opposed to
sequential systems  are systems capable of performing
different activities at the same time.
Semantics is the study of the meaning of words.
In concurrency, one often employs formal languages for the
description of concurrent systems. These I call system
description languages. Like all formal languages, system
description languages are usually introduced to avoid the
ambiguities of natural languages and to gain accuracy of expression.
Therefore their semantics tends to be easier than the semantics of
natural languages. Moreover the meaning of the words in a formal
language should to some extent be given by the one who defines the
language, rather than to be discovered by linguists.
Since system description languages tend to describe abstractions
of systems rather than concrete systems, the meaning of an expression
in a system description language is in general given by an
equivalence class of systems (i.e. a class of systems which are
considered to be equivalent on a chosen level of abstraction).
Thus the meaning of the entire language is determined by a partition
of a set of systems into equivalence classes and an allocation of one
such equivalence class to each expression. For this reason it is
convenient to divide the semantics of system description languages
into two subfields, namely the study of equivalence relations on sets
of concurrent systems, and the study of allocating
equivalence classes to expressions in particular languages.
The first field deals with the establishment of criteria, determining
when two systems are sufficiently alike to be collected in the same
equivalence class. It can be studied independently of a particular
system description language. Therefore it can be simply referred to as
semantics of concurrent systems or concurrency semantics
for short.
In concurrency semantics a criterion, determining when two systems are
sufficiently alike to be collected in the same equivalence class, is
called a semantics, and the induced equivalence relation a
semantic equivalence. In the literature on concurrency semantics
many semantics have been proposed and most likely also a multitude of
sensible semantics have never been proposed. The classification of
these semantics is called comparative concurrency semantics
and will be the primary subject of this thesis.
2. Design and verification
Much work in concurrency is motivated by an interest in design problems
for concurrent systems. A fruitful method to design concurrent systems
is by means of stepwise refinement. Here one starts with a
description S0 of the system one has in mind. This initial
description is called a specification of the desired system.
It abstracts from all the details of the desired system that are not
essential in its behaviour and leaves open many design decisions that
have to be taken later on. Then one starts refining the specification
by adding step for step the details one needs to know when the system is
going to be built. In this way one obtains a sequence
S0 > S1 > ... > Sn
of system descriptions of which the last one says exactly how the system
will look like. This final state in the design process describes the
implementation of the desired system.
Roughly one can distinguish two different kinds of refinement steps in
such a sequence of system descriptions. First of all there are steps
in which information is added about what the system ought to do.
These steps concern the goal of the entire exercise and can therefore
not be proven correct in terms of this goal. Secondly there are steps
that add information about how the system is going to do it.
It is one of the tasks of concurrency theory to prove the correctness of
such steps.
When considering only one step from a stepwise refinement sequence,
the lefthand side of this step is called specification and the
righthand side implementation. Let S > I be a `how'step.
The question is now to find criteria for determining whether or not this
step is correct. Here at least two situations can be distinguished:

Although I describes much more activities of the desired system than
S, all these extra activities can be considered as internal actions
in which the user of the system is not interested. After abstraction
from all these details, I and S are equivalent according to some
suitable semantic equivalence.

Some choices about how the final system should behave, that were left
open in S, are resolved in I. Therefore I and
S cannot be equivalent. Here one needs a partial order between
equivalence classes of concurrent systems, specifying when one system
is a correct implementation of the other.
In order to tackle both cases one needs to define a suitable semantic
equivalence and a partial order on the equivalence classes. Together
these ingredients can be coded as a preorder, a reflexive and
transitive relation, on system descriptions.
In this thesis, for reasons of convenience, attention is restricted to
equivalences rather than arbitrary preorders. However, there exists a
close correspondence between semantic equivalences and preorders.
Most semantic equivalences are defined, or can be characterized, in
terms of the properties that are shared by equivalent systems. For each
system p, a set of properties O(p) is defined, such that
two systems p and q are equivalent iff O(p) = O(q).
Often O(p) describes the observable behaviour of p
according to some testing scenario. Now a corresponding preorder
<< can be defined by p << q iff O(p) is a
subset of O(q). Most preorders encountered in the literature on
concurrency are of that form. I expect that using this insight,
much work on classifying semantic equivalences can be generalized to
preorders.
Above I argued that semantic equivalences (and preorders) can be relevant
for the design of concurrent systems. However, in fact they are more often
employed for verification purposes. In this case one is offered
a specification and an implementation of a certain system and is asked
to determine if the implementation is correct. In such applications
the distance between the specification and the implementation tends to
be larger than in one step in a design process. Therefore it is even
more important to have solid criteria for deciding on the correctness
of the implementation.
When semantic equivalences are used in the design of concurrent systems,
or for verification purposes, they should be chosen in such a way that
two system descriptions are considered equivalent only if the described
behaviours share the properties that are essential in the context in
which the system will be embedded. It depends on this context and on
the interests of a particular user which properties are essential.
Therefore it is not a task of concurrency semantics to find the `true'
semantic equivalence, but rather to determine which equivalence is
suitable for which applications. It is the intention of this thesis
to carry out a bit of this task. In particular it addresses the
question which semantic equivalences are suitable for dealing with
action refinement.
3. Refinement of actions
In this thesis concurrent systems are represented by expressions in a
system description language or by elements of some mathematical model.
The basic building blocks in the languages and models that occur in this
thesis are the actions which may be performed by a system. By an
action here any activity is understood which is considered as a
conceptual entity on a chosen level of abstraction. This allows design
steps in which actions are replaced by more complex system
descriptions. Such a step in the design of a system is referred to as
refinement of actions. This thesis deals with uniform
concurrency only, meaning that the actions are represented by
uninterpreted symbols a,b,c,... that are almost treated like
variables.
(In particular, the convention applies that different occurrences
of the same action a are to be refined in the same way. In other
words, when the possibility exists that two activities in a
specification are going to be implemented differently, they should be
given different names.)
In this context, action refinement should be regarded as a design step that
adds information about what the system ought to do (a `what'step), at
least if the refined actions are not considered to be internal.
Therefore the `correctness' of such refinement steps
cannot be proven.
However, the possibility of doing such steps puts some restrictions on
the kind of equivalences that can be used for proving the correctness of
`how'steps occurring in the same design process.
Example: Consider the following specification of a concurrent system:
`The actions a and b should in principle be performed
independently on different processors, but if one of the processors
happens to be ready with a before the other starts with
b, b may also be executed on this processor instead of
the other one'. This system description is represented by
the Petri net K.
An introduction to Petri nets and the way they model concurrent systems
can be found in
Reisig: Petri Nets  An Introduction, EATCS Monographs
on Theoretical Computer Science 4, SpringerVerlag, 1985,
or
Peterson: Petri Nets, ACM Computing Surveys 9(3), pp.
223252, 1981.
Suppose that someone comes up with an implementation in which first
it is determined whether the actions a and b will happen
sequentially or independently, and subsequently one of these
alternatives will take place, as represented by the Petri net L.
Although this implementation does not seem very convincing, it will be
considered `correct' by many equivalences occurring in the literature.
Let the next step in the design process consist of refining the action
a into the sequential composition of two actions a1 and
a2. From L one thereby obtains the net L'.
If L' is going to be placed in an environment where a2 becomes
causally dependent on b  it may be the case that b is an output
action, a2 is an input action, and the environment needs data
from b in order to compute the data that are requested by a2 
then deadlock can occur. However, if the refinement step splitting
a in a1 and a2 is carried out on K already, the
resulting system K' is deadlock free in the environment sketched
above.
Thus the possibility of refining a somehow invalidates the correctness
of the design step from K to L.
A semantic equivalence is said to be preserved under refinement of
actions if two equivalent processes remain equivalent after replacing
all occurrences of an action a by a more complicated process
r(a).
The example above indicates that for certain applications is may be
fruitful to employ equivalences that are preserved under refinement of
actions. It is one of the topics of this thesis to find out which
equivalences have this property.
4. About the contents of this thesis
This thesis consists of seven chapters which are all based on separate
papers and have their own introduction. This general introduction is
only meant to give an indication of their contents and their role in
the thesis.
In the first chapter several semantic equivalences for concrete
sequential systems are presented, and motivated in terms of the
observable behaviour of systems, according to some testing scenario.
Here concrete means that no internal actions or internal choice
are considered. These semantics are partially ordered by the relation
`makes strictly more identifications than', thus constituting a
complete lattice. For ten of these semantic equivalences complete axiomatizations
are provided. As in the rest of my thesis, stochastic
and realtime aspects of concurrent systems are completely neglected.
Chapter I serves partly to
give an overview of the literature on semantic equivalences for
concrete sequential processes. The various notions that can be found
elsewhere can easily be compared, since they are all presented in the
same style, and using the same formalism. In order for the semantics
of this chapter to be applicable for design and verification purposes,
they have to be generalized to a setting with internal moves, and
with parallelism. This can be done in many ways. In the last two chapters
the two extreme points on the semantic lattice, trace semantics and
bisimulation semantics, are generalized to a setting with parallelism
and in Chapter III, bisimulation semantics is generalized to a setting
with internal moves.
In the second chapter it is shown how semantic notions can be used
in protocol verification and other applications. This chapter is
entirely algebraic in style and employs axiom systems of which only
classes of models are considered, rather than a particular model.
It is based on the Algebra of Communicating Processes of
Bergstra & Klop: Process Algebra for Synchronous
Communication, I&C 60, pp. 109137, 1984.
In order to combine axiom systems representing semantic notions that
are difficult to combine a new notion of `proof' is developed.
The third chapter is devoted to the generalization of bisimulation
equivalence to a setting with silent moves. It is argued that the solution of
Milner: A Calculus of Communicating Systems, LNCS 92,
SpringerVerlag, 1980 (observation equivalence) does not respect the
branching structure of processes and hence lacks an important feature
of bisimulation semantics without internal moves. A finer equivalence
is proposed which indeed respects branching structure. This new
branching bisimulation equivalence turns out to
have some practical advantages as well. In particular, we show that in
a setting without parallelism it is preserved under refinement of
actions, whereas observation equivalence is not.
In the fourth chapter an operator for refinement
of actions is defined on four causality based models for concurrent
systems, namely on three kinds of event structures and on Petri nets,
and in the remaining three chapters it is investigated which of the
`linear time' and `branching time' semantic equivalences proposed in the
literature are preserved under refinement of actions and which are not.
Chapter V can be regarded as an informal summary of the Chapters VI and
VII. It uses Petri nets rather than event structures and contains no
technicalities like definitions and proofs. Instead more attention
has been paid to the examples.
All chapters in this thesis can be read independently, although
for motivation it may be helpful to read the introduction to Chapter IV
before Chapters VVII, and depending on the taste of the reader
it may be fruitful to consult Chapter V before or simultaneously with
the last two chapters. Furthermore Chapter VI depends on Section 1
or 2 of Chapter IV. Conceptually Chapter VII follows Chapter VI,
and it recalls its results.
The main new results contributed by this thesis and its
constituent papers are the following:

A short noncategorical proof showing that two processes are
bisimulation equivalent
if and only if they have the same representation in Aczel's universe
of nonwellfounded sets (Proposition 1.9 in Chapter I). This result
follows immediately from the categorical considerations in
Aczel: Nonwellfounded Sets, CSLI Lecture Notes No. 14,
Stanford University 1988,
but it is difficult to point out a precise spot in Aczel's text were
it is obtained.

Basically all semantics for concrete sequential processes found in the
literature that can be defined uniformly in terms of action relations
are presented in a uniform framework and motivated in terms of testing
scenarios (Chapter I, Section 1).

These semantics are partially ordered with respect to their
distinguishing power. (Theorems 2.1 and 2.9 for finitely branching
processes; Theorems 2.2 and 2.10 for infinitely branching processes.)

A complete axiomatization of completed trace equivalence on finite
closed process expressions (Theorem 3.1 in Chapter I).

Complete axiomatizations of simulation equivalence and ready
simulation equivalence on finite process expressions (Theorems 3.1 and
3.2).

The introduction of an algebraic specification technique with homomorphism
and subalgebra operators (Chapter II, Section 1).

A new logic with a new concept of proof for statements involving these
specifications (Chapter II, Section 1.8).

A concise overview of equational, conditional and first order logic
(Appendix to Chapter II).

A new formulation of the Recursive Specification Principle in
ACP (Theorem 2.8.2 in Chapter II) and more in general a concise
presentation of the module ACP# (Chapter II, Section 2).

The inconsistency of the law T4 ( tau ( tau x + y ) = tau x + y ) in
combination with ACP (Proposition 3.1.2.2). Equivalences in
which this law is valid fail to be congruences for the leftmerge
operator of ACP.

The application of our module logic to combine the leftmerge and T4
in ACP verifications (Section 3.1 in Chapter II).

The application of our specification technique to express an
associative chaining operator in ACP# (Section 3.2 in Chapter II).

The specification of several types of (faulty) queues and bags using
the chaining operator, and the verification of their basic properties
(Chapter II, Section 4). Thanks to the parametrized nature of our
specifications, many properties that we verified for the normal queue,
can be inferred to hold for the various faulty queues as well.

An example of a plausible identity concerning faulty queues that does
not hold in weak bisimulation semantics (Theorem 4.5.1). This identity
can be proved when the axiom T4 above is added to the axioms of
weak bisimulation semantics (Theorem 4.5.2).

A verification of the Concurrent Alternating Bit Protocol in no more
than 5 pages (Chapter II, Section 5).

The observation that observation equivalence (weak bisimulation) does
not respect branching time (Introduction to Chapter III).

The introduction of branching bisimulation equivalence as an
alternative (Chapter III, Section 1).

The stuttering lemma (1.1) saying that all intermediate states on a
taupath between two equivalent states are also equivalent with those
states. This lemma allows a simpler presentation of a branching
bisimulation.

The classification of etabisimulation and delay bisimulation as two
incomparable notions between weak and branching bisimulation (Section 1).

The characterization of rooted weak bisimulation equivalence as the
coarsest congruence for + finer than weak bisimulation equivalence, provided
that there is at least one action different from tau (Theorem 2.4 in
Chapter III). The proof does not use the Fresh Atom Principle and is
valid independent of possible cardinality restrictions imposed on the
space of processes to which it applies. The same proof also applies to
(rooted) branching bisimulation, etabisimulation and delay
bisimulation.

The introduction of coloured traces and consistent colourings, which
show how branching bisimulation equivalence preserves the branching
structure of processes (Section 3); the characterization of
(rooted) branching bisimulation equivalence as (rooted) coloured trace
equivalence (Th. 3.2).

The characterization of branching bisimulation equivalence as
hypertrace equivalence (Theorem 3.3).

The definition of a unique normal form in every branching bisimulation
congruence class, which constitutes a minimal representation of
branching congruent processes (Section 3, end).

An explanation of the way in which deadlock and termination are
treated in Basic Process Algebra (BPA), the Calculus of Communicating
Systems (CCS) and the Algebra of Communicating Processes (ACP)
(Section 2).

A complete axiomatization of branching bisimulation congruence on
finite closed process expressions. This is done for (essential parts
of) BPA, CCS as well as ACP (Sections 2 and 4).

Alternative completeness proofs for the known axiomatizations of weak,
eta and delay bisimulation congruence, based on a saturation
technique that reduces these congruences to branching congruence
(Section 4, end).

A simple proofrule that converts a complete axiomatization of rooted branching
bisimulation into one of unrooted branching bisimulation equivalence
(Theorem 2.15).
Such a rule was known already for weak bisimulation and also holds for
delay and etabisimulation.

The discovery that for a large class of processes weak and branching
bisimulation coincide, and that, as far as we know, all protocols that
have been verified in weak bisimulation semantics are also valid in
branching bisimulation semantics (Section 5).

The observation that (rooted) weak bisimulation equivalence is not
preserved under refinement of actions, even if only sequential
processes without interleaving operators are considered (Section 6).

The result that for sequential processes branching bisimulation is
preserved under action refinement (Theorem 6.1).

A method for obtaining a refinement theorem (like the one mentioned
above) directly from the complete axiomatization of an equivalence.

The definition of branching bisimulation preorders and equivalences
taking divergence into account, analogous to the existing preorders
and equivalences for weak bisimulation; and similarly for eta and
delay bisimulation (Section 7).

A sketch of a testing scenario for branching bisimulation equivalence
(Section 8, were also an overview of the work on modal
characterizations for branching bisimulation can be found). This
result was added in this second edition of my thesis.

A list of 11 arguments for choosing branching bisimulation semantics
in verifications and other applications of concurrency theory:

Verifications in branching bisimulation semantics are sound
independent of your notion of observable behaviour.

No coarser semantics (like weak bisimulation) has this property.

In abstract interleaving semantics no finer notion of bisimulation is
suitable.

There is a reasonable operator for which branching bisimulation is a
congruence and weak bisimulation or coarser notions are not. On the
other hand no examples testifying for the opposite are known.

Branching bisimulation equivalence is the only known equivalence in
the linear time  branching time spectrum that supports an
`eventually' operator as part of a temporal logic on transition
systems. It even supports all the operators of CTL* and
corresponds with stuttering equivalence of kripke structures.

There are practical applications in which weak bisimulation poses a
problem that can be solved by moving to branching bisimulation.
No applications have been found in which the reverse holds.

Branching bisimulation equivalence has a lower complexity than any
other abstract semantic equivalence used in concurrency theory.

Branching bisimulation is preserved under action refinement, whereas
weak bisimulation is not.

Branching congruence has a very appealing complete axiomatization

and better term rewriting properties than other (abstract) bisimulations.

And it has a nice characterization as backandforth bisimulation.
(Conclusion to Chapter III; arguments 2, 3, 4 and 6b were added in the
second edition; arguments 5b, 7, 11 and part of 4 depend on work by others).

An illustration of how action refinement can be used in the topdown design of
concurrent systems (Introduction to Chapter IV).

An argument against the use of forgetful refinements (refining an
action by the empty process, implemented by erasure) for this purpose
(ibidem).

The definition of an operator on prime event structures for refinement
of actions by nonempty, finite, conflictfree processes (Section 1).
It is established that this operator is welldefined up to isomorphism
(Prop. 1.5) and compositional w.r.t. configuration semantics
(Proposition 1.7).

The observation that prime event structures are less suitable for
refinement by conflicting or infinite behaviours (Section 1).

The modelling of deadlock behaviour and sequential composition of
flow event structures (Section 2).

The definition of an operator for general action refinement on flow
event structures, generalizing the one we had on prime event structures
(Section 2). It is established that this operator is welldefined up
to isomorphism (Prop. 2.7) and compositional w.r.t.
configuration semantics (Prop. 2.8).

The introduction of configuration structures as a model for
concurrency (Section 3). They are essentially just Winskel's families
of configurations of general event structures. The new name merely
reflects our opinion that they form a pleasant model of concurrency
even without considering event structures.

The observation that the infinite configurations in configuration
structures (or families of configurations) are redundant, and can
better be left out.

The definition of an operator for action refinement on configuration
structures (Section 3). It is established that this operator is
welldefined up to isomorphism (Proposition 3.7) and for deadlockfree
refinements agrees with the one on flow event structures (Theorem 3.8).

A construction for refinement of transitions in Petri nets, generalizing
similar constructions proposed earlier (Section 4). For occurrence nets
we establish that the construction is consistent with our operator for action
refinement on prime event structures (Theorem 4.18).

We show that several prospective generalizations of our approach do not
work.

The comparison of our notion of transition refinement with the notions of
(vicinity respecting) net morphism and quotient (Section 4).

An example showing that preservation of semantic equivalence of
processes under action refinement can be a useful property in
applications (this introduction).

Counterexamples showing that, besides the interleaving equivalences,
also none of the known step equivalences is preserved under action
refinement (Chapter V and Section 2 of Chapter VI).

A formal proof that linear time partial order semantics is preserved
under action refinement (Section 3 of Chapter VI).

Counterexamples showing that pomset bisimulation equivalence,
generalized pomset bisimulation equivalence, NMS partial ordering
equivalence, and a combination of those, are not preserved under
refinement of actions (Chapter V and Section 4 of Chapter VI).

The discovery that NMS partial ordering equivalence is incomparable
with pomset bisimulation equivalence, and the proposal of a
modification of this equivalence, which we call history
preserving bisimulation equivalence, that is finer then both, and
still satisfies the absorption laws (Section 4.2 of Chapter VI).
This notion was earlier proposed in a different model as behavior
structure equivalence. We argue that it is the coarsest equivalence
that models the interplay of causality and branching in full detail
(Conclusion to Chapter VI).

The result that history preserving bisimulation is preserved
under action refinement (Section 4.2 of Chapter VI).

The result that for systems without autoconcurrency history
preserving bisimulation and NMS partial ordering equivalence coincide
(ibidem).

An example strongly suggesting that history preserving bisimulation is
not the coarsest equivalence refining pomset bisimulation and being
preserved under action refinement (Conclusion to Chapter VI).

An overview of equivalence notions for concurrent systems (Chapters V,
VI and especially VII).

The introduction of STconfigurations to model the global state of an
event structure, just as STmarkings modal the global state of a Petri
net. I argue that when actions are allowed to have duration, they do
so better than ordinary markings or configurations (Chapter VII,
Section 4).

Several characterizations of STtrace and STbisimulation equivalence
on event structures (Section 5). STbisimulation had already been
defined on Petri nets, and STtrace equivalence is obtained as its
linear time variant.

The results that STtrace and STbisimulation equivalence are
preserved under refinement of actions (Section 6). It follows that
partial order semantics is not needed for dealing with action
refinement (Chapters V and VII).

An example showing that STbisimulation is not preserved under
forgetful refinement (Conclusion to Chapter VII).

The conjecture that STbisimulation is the coarsest equivalence
contained in bisimulation equivalence, and similarly STtrace the
coarsest in trace equivalence, that is preserved under action
refinement. Also the main idea for the proof is provided (ibidem).