Comparative Concurrency Semantics and Refinement of Actions

Academisch Proefschrift

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

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

Affiliations

Support

Prior Publications

Acknowledgements

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.

Introduction

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

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

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 3.1.2.2). 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).