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

Promotoren: prof. dr. J.W. Klop and prof. dr. J.A. Bergstra
Referent: prof. dr. G. Winskel


Introduction 7
  1. The linear time - branching time spectrum 17
    1. Semantic equivalences on labelled transition systems 22
    2. The semantic lattice 38
    3. Complete axiomatizations 50
  2. Modular specifications in process algebra - with curious queues 55
    1. Module logic 61
    2. Process algebra 66
    3. Applications of the module approach in process algebra 80
    4. Queues 89
    5. A protocol verification 102
    Appendix: Logics 111
  3. Branching time and abstraction in bisimulation semantics 117
    1. Branching and abstraction 120
    2. Axioms 130
    3. Branches and traces 143
    4. Completeness proofs 149
    5. Correspondence 158
    6. Refinement 159
    7. Divergence 163
    8. Modal characterizations 164
  4. Refinement of actions in causality based models 173
    1. Refinement of actions in prime event structures 181
    2. Refinement of actions in flow event structures 186
    3. Configuration structures and refinement of actions 193
    4. Refinement of transitions in Petri nets 197
  5. Partial order semantics for refinement of actions - neither necessary nor always sufficient but appropriate when used with care - 213
  6. Equivalence notions for concurrent systems and refinement of actions 223
    1. Interleaving semantics 225
    2. Step semantics 227
    3. `Linear time' partial order semantics 230
    4. `Branching time' partial order semantics 231
  7. The refinement theorem for ST-bisimulation semantics 243
    1. Concurrent systems and refinement of actions 247
    2. The behaviour of concurrent systems I 249
    3. Equivalence notions for concurrent systems I 250
    4. The behaviour of concurrent systems II 255
    5. Equivalence notions for concurrent systems II 257
    6. The refinement theorems 265
References 273


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, D-8000 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, D-5205 Sankt Augustin 1. My current affiliation is: Computer Science Department, Stanford University, CA 94305-9045, USA.


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 N00014-92-J-1974. 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].


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 Ernst-Rü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, Fer-Jan 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 left-hand side of this step is called specification and the right-hand 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:

  1. 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.
  2. 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, Springer-Verlag, 1985, or Peterson: Petri Nets, ACM Computing Surveys 9(3), pp. 223-252, 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 real-time 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. 109-137, 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, Springer-Verlag, 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 V-VII, 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.

5. Results

The main new results contributed by this thesis and its constituent papers are the following:
  1. A short non-categorical proof showing that two processes are bisimulation equivalent if and only if they have the same representation in Aczel's universe of non-well-founded sets (Proposition 1.9 in Chapter I). This result follows immediately from the categorical considerations in Aczel: Non-well-founded 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.
  2. 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).
  3. 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.)
  4. A complete axiomatization of completed trace equivalence on finite closed process expressions (Theorem 3.1 in Chapter I).
  5. Complete axiomatizations of simulation equivalence and ready simulation equivalence on finite process expressions (Theorems 3.1 and 3.2).
  6. The introduction of an algebraic specification technique with homomorphism and subalgebra operators (Chapter II, Section 1).
  7. A new logic with a new concept of proof for statements involving these specifications (Chapter II, Section 1.8).
  8. A concise overview of equational, conditional and first order logic (Appendix to Chapter II).
  9. 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).
  10. The inconsistency of the law T4 ( tau ( tau x + y ) = tau x + y ) in combination with ACP (Proposition Equivalences in which this law is valid fail to be congruences for the left-merge operator of ACP.
  11. The application of our module logic to combine the left-merge and T4 in ACP verifications (Section 3.1 in Chapter II).
  12. The application of our specification technique to express an associative chaining operator in ACP# (Section 3.2 in Chapter II).
  13. 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.
  14. 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).
  15. A verification of the Concurrent Alternating Bit Protocol in no more than 5 pages (Chapter II, Section 5).
  16. The observation that observation equivalence (weak bisimulation) does not respect branching time (Introduction to Chapter III).
  17. The introduction of branching bisimulation equivalence as an alternative (Chapter III, Section 1).
  18. The stuttering lemma (1.1) saying that all intermediate states on a tau-path between two equivalent states are also equivalent with those states. This lemma allows a simpler presentation of a branching bisimulation.
  19. The classification of eta-bisimulation and delay bisimulation as two incomparable notions between weak and branching bisimulation (Section 1).
  20. 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, eta-bisimulation and delay bisimulation.
  21. 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).
  22. The characterization of branching bisimulation equivalence as hypertrace equivalence (Theorem 3.3).
  23. 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).
  24. 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).
  25. 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).
  26. 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).
  27. A simple proof-rule 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 eta-bisimulation.
  28. 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).
  29. 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).
  30. The result that for sequential processes branching bisimulation is preserved under action refinement (Theorem 6.1).
  31. A method for obtaining a refinement theorem (like the one mentioned above) directly from the complete axiomatization of an equivalence.
  32. 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).
  33. 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.
  34. A list of 11 arguments for choosing branching bisimulation semantics in verifications and other applications of concurrency theory:
    1. Verifications in branching bisimulation semantics are sound independent of your notion of observable behaviour.
    2. No coarser semantics (like weak bisimulation) has this property.
    3. In abstract interleaving semantics no finer notion of bisimulation is suitable.
    4. 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.
    5. 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.
    6. 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.
    7. Branching bisimulation equivalence has a lower complexity than any other abstract semantic equivalence used in concurrency theory.
    8. Branching bisimulation is preserved under action refinement, whereas weak bisimulation is not.
    9. Branching congruence has a very appealing complete axiomatization
    10. and better term rewriting properties than other (abstract) bisimulations.
    11. And it has a nice characterization as back-and-forth 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).
  35. An illustration of how action refinement can be used in the top-down design of concurrent systems (Introduction to Chapter IV).
  36. An argument against the use of forgetful refinements (refining an action by the empty process, implemented by erasure) for this purpose (ibidem).
  37. The definition of an operator on prime event structures for refinement of actions by non-empty, finite, conflict-free processes (Section 1). It is established that this operator is well-defined up to isomorphism (Prop. 1.5) and compositional w.r.t. configuration semantics (Proposition 1.7).
  38. The observation that prime event structures are less suitable for refinement by conflicting or infinite behaviours (Section 1).
  39. The modelling of deadlock behaviour and sequential composition of flow event structures (Section 2).
  40. 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 well-defined up to isomorphism (Prop. 2.7) and compositional w.r.t. configuration semantics (Prop. 2.8).
  41. 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.
  42. The observation that the infinite configurations in configuration structures (or families of configurations) are redundant, and can better be left out.
  43. The definition of an operator for action refinement on configuration structures (Section 3). It is established that this operator is well-defined up to isomorphism (Proposition 3.7) and for deadlock-free refinements agrees with the one on flow event structures (Theorem 3.8).
  44. 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).
  45. We show that several prospective generalizations of our approach do not work.
  46. The comparison of our notion of transition refinement with the notions of (vicinity respecting) net morphism and quotient (Section 4).
  47. An example showing that preservation of semantic equivalence of processes under action refinement can be a useful property in applications (this introduction).
  48. 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).
  49. A formal proof that linear time partial order semantics is preserved under action refinement (Section 3 of Chapter VI).
  50. 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).
  51. 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).
  52. The result that history preserving bisimulation is preserved under action refinement (Section 4.2 of Chapter VI).
  53. The result that for systems without autoconcurrency history preserving bisimulation and NMS partial ordering equivalence coincide (ibidem).
  54. 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).
  55. An overview of equivalence notions for concurrent systems (Chapters V, VI and especially VII).
  56. The introduction of ST-configurations to model the global state of an event structure, just as ST-markings 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).
  57. Several characterizations of ST-trace and ST-bisimulation equivalence on event structures (Section 5). ST-bisimulation had already been defined on Petri nets, and ST-trace equivalence is obtained as its linear time variant.
  58. The results that ST-trace and ST-bisimulation 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).
  59. An example showing that ST-bisimulation is not preserved under forgetful refinement (Conclusion to Chapter VII).
  60. The conjecture that ST-bisimulation is the coarsest equivalence contained in bisimulation equivalence, and similarly ST-trace the coarsest in trace equivalence, that is preserved under action refinement. Also the main idea for the proof is provided (ibidem).