A Complete Axiomatization for Branching Bisimulation Congruence of Finite-State Behaviours

R.J. van Glabbeek^{∗}

Computer Science Department, Stanford University Stanford, CA 94305, USA.

                                     rvg@cs.stanford.edu

This paper offers a complete inference system for branching bisimulation congruence on a basic sublanguage of CCS for representing regular processes with silent moves. Moreover, complete axiomatizations are provided for the guarded expressions in this language, representing the divergence-free processes, and for the recursion-free expressions, representing the finite processes. Furthermore it is argued that in abstract interleaving semantics (at least for finite processes) branching bisimulation congruence is the finest reasonable congruence possible. The argument is that for closed recursion-free process expressions, in the presence of some standard process algebra operations like partially synchronous parallel composition and relabelling, branching bisimulation congruence is completely axiomatized by the usual axioms for strong congruence together with Milner’s first τ-law aτX = aX.

Contents

1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 2 A language for finite-state behaviours . . . . . . . . . . . . . . . . . . . . . . . . . . 3 3 Branching bisimulation congruence . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 4 The axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 5 Completeness for guarded process expressions . . . . . . . . . . . . . . . . . . . . . . 10 6 Completeness for finite process expressions . . . . . . . . . . . . . . . . . . . . . . . 12 7 Completeness for all process expressions . . . . . . . . . . . . . . . . . . . . . . . . . 13 8 Concluding remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

1 Introduction

An important class of mathematical models for concurrent systems are the term models, in which a process or behaviour (of a system) is represented as a congruence class of expressions in a system description language. The best known system description language is Milner’s Calculus of Communicating Sytems (CCS), and the best known congruence on CCS expressions^{1} is bisimulation congruence [7]. The choice of bisimulation congruence was originally motivated by a notion of observability: “processes are equal iff they are indistinguishable by any experiment based on observation” [7]. However, since the appearance of bisimulation congruence, many alternative notions of observability, or testing scenarios, have been proposed, all leading to different—and invariably coarser—congruences. See Van Glabbeek [3] for an overview. What makes bisimulation congruence special among all these alternatives is not so much the underlying notion of observation, but the fact that it is the finest reasonable congruence. To be precise, this is the case in interleaving semantics, where the “concurrent occurrence of two observable actions is not distinguished from their occurrence in arbitrary sequence” [7]. In non-interleaving semantics one finds finer congruences, but the finest ones are just variations of bisimulation congruence that take causal dependence between action occurrences explicitly into account. What makes bisimulation congruence the finest reasonable congruence are two properties:

∗This work was supported by ONR under grant number N00014-92-J-1974.

1In this first paragraph I restrict myself to expressions that model behaviours without hidden moves (τ-actions).

• Any two bisimilar process expressions have the same internal structure, to be precise the same branching structure. As the observable behaviour of processes according to any alternative (interleaving based) testing scenario is completely determined by their branching structure, it follows that other observable congruences must be coarser.

• Finer equivalences than bisimulation congruence (such as tree equivalence or graph isomorphism) suffer from serious drawbacks such as a higher complexity (to decide the equivalence of finite-state behaviours) and the inequivalence of standard operational and denotational interpretations of CCS-like system description languages.

A crucial tool in practical applications of system description languages like CCS, especially for verification purposes, is an abstraction mechanism. Abstraction is usually performed by turning actions that are considered unimportant into the invisible action τ. Then, a system that after some activity reaches a state from which only an invisible action is possible, leading to another state, is considered equivalent to an otherwise identical system, that after said activity immediately reaches the other state. Thus the mechanism of abstraction by hiding of irrelevant or unobservable actions needs support from the congruence notion employed.

There are many ways to extend bisimulation congruence to processes with hidden moves. The simplest generalization is strong (bisimulation) equivalence, in which τ-actions are treated no different than visible actions. For this reason strong congruence is not abstract in the sense stipulated above. Another option is to take the testing scenario underlying bisimulation equivalence as primary, incorporating the unobservable nature of hidden moves. This yields Milner’s notion of weak (bisimulation) congruence [7], also called observation congruence, in spite of the rather far-going assumptions about the capabilities of observers that need to be made for weak congruence to be truly observable. In Van Glabbeek & Weijland [4] another generalization of bisimulation congruence was proposed. Branching (bisimulation) congruence is not so much motivated in terms of its testing scenario (although it has one that is arguably only twice as contrived as that of weak bisimulation congruence), but generalizes the property of bisimulation congruence of being the finest reasonable interleaving congruence to an abstract setting. To be precise: it preserves the branching structure of processes (unlike weak congruence) [4], and (at least for finite processes) any finer or incomparable abstract version of bisimulation congruence violates the expansion theorem [7], that is characteristic for interleaving semantics.

Besides a substantiation of the last claim, this paper offers a complete axiomatization of branching bisimulation congruence for a sublanguage BCCS^{ω} of CCS, only containing operators for action, inaction, choice and recursion. The B stands for Basic and ω is a strict upper bound for the number of arguments of the choice and recursion operators. This language represents all and only the regular processes or finite-state behaviours. Moreover, complete axiomatizations for two sublanguages are given: the language of recursion-free BCCS^{ω} expressions, representing the finite processes, and the language of guarded BCCS^{ω} expressions, representing the divergence-free processes, where a processes is divergent if it has a state from which an infinite sequence of hidden moves is possible.

A complete axiomatization for strong congruence on BCCS^{ω} was provided in Milner [5]. It consisted of the axioms E1-4, A0-3 and R1-3 of Section 4 (as well as α-conversion, which is derivable). A complete axiomatization for weak congruence on a slightly different language was first provided in Bergstra & Klop [2]. A more aesthetic axiomatization (on BCCS^{ω}), partly inspired by the one in [2], was given in Milner [6]. It consisted of the axioms for strong congruence, 3 so-called τ-laws, and 2 extra axioms for unguarded recursion (besides R3). The present axiomatization counts, besides the axioms for strong congruence, only one τ-law, but 3 extra axioms for unguarded recursion (all weaker than the axioms for weak congruence). In all three cases the axioms for unguarded recursion can be dropped to obtain complete axiomatizations for guarded expressions, and on top of that R1 and R2 can be dropped to obtain complete axiomatizations for finite processes.

Milner’s completeness proof was delivered in five steps:

(a) Any expression can be converted into a guarded one.

(b) Any guarded expression provably satisfies a standard guarded set of equations.

(c) Any standard guarded set of equations can be converted into a saturated one (preserving the property of being provably satisfied by an expression).

(d) Two congruent processes that each provably satisfy a saturated standard guarded set of equations, provably satisfy a common guarded set of equations.

(e) If two guarded expressions satisfy the same guarded set of equations, they are provably equal.

Steps (b) and (e) only use the axioms for strong congruence, and can thus be applied in the setting of branching bisimulation as well. Step (a) can be made completely analogous, even though the present axioms for unguarded recursion are much more complicated (in particular, the side-condition of R4 can not be eliminated, as could be done for the corresponding axiom R5 in [6]). Step (c) must be skipped as saturation is unsound in branching bisimulation semantics, and therefore step (d) needs to be made more subtle. But the absence of step (c) makes it possible to incorporate step (b) into step (d) at no extra cost.

The completeness theorem for branching congruence on recursion-free process expressions, at least the closed ones, was already proven in [4] by the method of graph transformations, due to Bergstra & Klop [1]. The present proof is distinctly shorter. On the other hand, the method of graph transformations, once mastered, tends to deliver completeness proofs on finite closed terms for arbitrary interleaving equivalences almost instantaneously, whereas the method used here seems rather bisimulation oriented and requires more thought.

2 A language for finite-state behaviours

Let the nonempty set A of visible actions and the disjoint infinite set V of variables be given. Let τ ∉ A be the invisible action or hidden move and write A_{τ} = A ∪ {τ}.

Definition 1 The set E of process expressions over BCCS^{ω} is given by

X  ∈ E for X ∈ V  (variable)
0  ∈ E  (inaction)
aE  ∈ E for a ∈ A_{τ} and E ∈ E (action)
E + F ∈ E for E, F ∈ E  (choice)
μXE ∈ E for X ∈ V_{S} and E ∈ E (recursion)

The expression 0 represents a process that is unable to perform any action. aE represents a process that first performs the action a and then proceeds as E. E +F represents a process that will behave as either E or F, and μXE represents a solution of the equation X = E.

Definition 2 An occurrence of a variable X in an expression E ∈ E is bound if it occurs in a subexpression of the form μXF. Otherwise it is free. E is open if it contains a free occurrence of a variable, and closed otherwise. E{F/X} denotes the result of substituting F for all free occurrences of X in E, if necessary^{2} renaming bound variables in E in order to ensure that no free occurrence of a variable in F becomes bound in E{F/X}. Likewise E{E_{X}/X}_{X∈V′}, for V′ ⊆ V, denotes the result of simultaneously substituting E_{X} for X in the same fashion.

Definition 3 The transition relation ⟶⊆ E × (A_{τ} ∪ V) × E is the smallest relation satisfying

• X ⟶^{X} 0 for X ∈ V

• aE ⟶^{a} E for a ∈ A_{τ}

• if E ⟶^{x} G or F ⟶^{x} G then E + F ⟶^{x} G

• if E{μXE/X} ⟶^{x} F then μXE ⟶^{x} F

Here E ⟶^{a} F for a ∈ A_{τ} means that the system represented by E can perform the action a, thereby evolving into F, and E ⟶^{X} 0 means that the system represented by E has the possibility to continue as whatever system is substituted for the variable X.

Definition 4 Let E ∈ E. The set E_{E} of process expressions reachable from E is defined as the smallest subset of E satisfying E ∈ E_{E} and if F ⟶^{a} G with a ∈ A_{τ} and F ∈ E_{E} then G ∈ E_{E}.

Proposition 1 E_{E} is finite for E ∈ E.

Proof: Consider the transition relation →⊆ E′ × (A_{τ} ∪^{·} {+, μ}) × E′, given by

• aE →^{a} E

• E + F →^{+} E and E + F →^{+} F

• μXE →^{μ} E{μXE/X}

2Renaming is necessary if a free occurrence of X appears in a subterm μY G of E with Y occurring free in F.

Here E′ is defined as E, except that every operator symbol (X, 0, a, +, μX) in an expression E ∈ E′ is coloured either red or black. Furthermore, if in a subexpression aF, F + G or μXF of E the leading operator a, + or μX is coloured black, the entire subexpression must be black. Whether an occurrence of a variable is free or bound does not depend on its colour. Substitution on E′ is defined such that E{F/X} means E{black(F)/X} (i.e. a black version of F is substituted for any free red or black occurrence of X), and renaming of bound variables doesn’t change their colour. Furthermore colours are preserved under transitions.

Choose E ∈ E and let E′_{E} be the set of coloured expressions in E′ that are reachable by → from red(E). If F ⟶^{a} F′ for F, F′ ∈ E, and F_{0} ∈ E′ is a coloured version of F, then there must be

F_{1},…, F_{n+1} ∈ E′ with n ∈ IN such that F_{i−1} →^{+} F_{i} or F_{i−1} →^{μ} F_{i} for i = 1,…, n, F_{n} →^{a} F_{n+1} and

F_{n+1} is a coloured version of F′. Thus for any F ∈ E_{E} a coloured version appears in E′_{E}, and it suffices to proof that E′_{E} is finite, or becomes finite after forgetting the colours.

Observe that if an expression F is partly red and F → F′ then the red part of F′ is smaller than the red part of F. Thus there are only finitely many expressions in E′_{E} that are partly red.

Furthermore observe that for any F ∈ E′_{E}, if F contains a subexpression μY G with μY red, then no black subexpression of G contains a free occurrence of Y. This property is trivially true for red(E), trivially preserved under →^{a} and →^{+}, and preserved under →^{μ} by the renaming-of-bound-variables convention of Definition 2. It follows that if F ∈ E′_{E} is partly red and F → F′, then the black subexpressions of F that are inherited by F′—unlike the red ones—are unchanged in F′. Thus if H ∈ E′_{E} is partly red, H → H′ and H′ is completely black, then H′ has the form μXG and has been generated by a derivation μXG →^{μ} G{μXG/X}. Hence the black term H = μXG ∈ E′_{E} also occurs as a partly red term μXG ∈ E′_{E}.

It follows that E_{E} is finite. In fact E_{E} contains at most one element more than it has subexpressions of the form aF. □

Definition 5 A free occurrence of a variable X in an expression E ∈ E is guarded if it occurs in a subexpression of the form aF with a ∈ A (i.e. a ≠ τ). X is (un)guarded in E if (not) every free occurrence of X in E is guarded. A process expression E ∈ E is guarded if for every subexpression μXF, X is guarded in F. Let E^{g} ⊆ E be the set of guarded process expressions over BCCS^{ω}.

Definition 6 A process expression E ∈ E is called finite or, more accurately, recursion-free if it has no subexpression of the form μXF. Let E^{f} ⊆ E^{g} ⊆ E be the set of finite process expressions over BCCS^{ω}.

Lemma 1 If E ∈ E^{f}, then the relation ⟶ is well-founded in E_{E}. This means that there are no

F_{i} ∈ E_{E} and a_{i} ∈ A_{τ} for i ∈ IN with F_{i} ⟶^{a_{i}} F_{i+1} for i ∈ IN.

Proof: If F ∈ E^{f} and F ⟶^{a} F′ then F′ ∈ E^{f} and F′ is smaller than F. □

Lemma 2 If E ∈ E^{g}, then the relation ⟶^{τ} is well-founded in E_{E}.

Proof: First note that if E is guarded and F ∈ E_{E} then F is guarded. This follows with a straightforward induction on derivations. For F ∈ E, let F^{∗} be F, in which every occurrence of a subterm aG with a ∈ A is replaced by 0. Note that if F is guarded then F^{∗} is guarded, and if F ⟶^{τ} G then F^{∗} ⟶^{τ} G^{∗}. Now suppose there is an infinite path F_{0} ⟶^{τ} F_{1} ⟶^{τ} F_{2} ⟶^{τ} ⋯ as denied in the lemma. Then there must be an infinite path F_{0}^{∗} ⟶^{τ} F_{1}^{∗} ⟶^{τ} F_{2}^{∗} ⟶^{τ} ⋯, only passing through guarded process expressions without subexpressions of the form aG for a ∈ A. But if H is such an expression and H ⟶^{τ} H′, then H′ is smaller than H, yielding a contradiction. □

Write E ⟹ E′ if there are E_{0},…, E_{n} ∈ E with E = E_{0} ⟶^{τ} E_{1} ⟶^{τ} ⋯ ⟶^{τ} E_{n} = E′.

Lemma 3 X ∈ V is unguarded in E ∈ E iff E ⟹ E′ ⟶^{X} 0. Proof: Straightforward. □

Definition 7 Renaming of bound variables is called α-conversion. Write E =_{α} F if E, F ∈ E only differ by α-conversion.

Lemma 4 Let x ∈ A_{τ} ∪ V.

1. H ⟶^{X} 0 ∧ E ⟶^{x} F ⇒ H{E/X} ⟶^{x} F

2. H ⟶^{x} H′ ∧ x ≠ X ⇒ H{E/X} ⟶^{x} H′′{E/X} with H′ =_{α} H′′

3. H{E/X} ⟶^{x} F ⇒ (H ⟶^{X} 0 ∧ E ⟶^{x} F) ∨ (x ≠ X ∧ H ⟶^{x} H′ =_{α} H′′ ∧ F = H′′{E/X})

Proof: 1. and 2. are straightforward by induction on inference. I will prove 3. by induction on the inference of H{E/X} ⟶^{x} F. In case H = X the first alternative applies: H ⟶^{X} 0 ∧ E ⟶^{x} F. The cases F = Y ≠ X, H = aG, H = H_{1} + H_{2} and H = μXG are straightforward, so assume H = μY G with Y ≠ X. Let H̃ = μỸ G̃ be the result of renaming bound variables in H, as described in Definition 2. Now, by a shorter inference G̃{E/X}{H̃{E/X}/Ỹ } = G̃{H̃/Ỹ }{E/X} ⟶^{x} F, so by induction (H̃ ⟶^{X} 0 ∧ E ⟶^{x} F) ∨ (x ≠ X ∧ H̃ ⟶^{x} H̃′ =_{α} H′′ ∧ F = H′′{E/X}), from which the desired conclusion follows. □

3 Branching bisimulation congruence

Definition 8 A branching bisimulation is a symmetric relation R ⊆ E × E such that ∀x ∈ A_{τ} ∪ V:

if (E, F) ∈ R ∧ E ⟶^{x} E′ then \begin{matrix}x = τ and (E′, F) ∈ R \\ or ∃F′′, F′ : F ⟹ F′′ ⟶^{x} F′ ∧ (E, F′′) ∈ R ∧ (E′, F′) ∈ R. \end{matrix}

Two expressions E and F are branching (bisimulation) equivalent—notation E \underline{↔}_{b} F —if there exists a branching bisimulation R with (E, F) ∈ R.

For further motivation of branching bisimulation equivalence see Van Glabbeek & Weijland [4]. The consise definition above is possible thanks to the following lemma.

Lemma 5 If E \underline{↔}_{b} F, E \underline{↔}_{b} F′′ and F ⟹ F′′, then E \underline{↔}_{b} F′ for any F′ with F ⟹ F′ ⟹ F′′. Proof: In [4]. □

It is more common to use Definition 8 for closed process expressions only, thereby avoiding the use of the transitions ⟶^{X}, and to extend the definition to open process expressions by

E \underline{↔}_{b} F iff for all closed process expressions G, E\{G/X\}\underline{↔}_{b} F \{G/X\}

By Propositions 2 and 3 below both approaches yield the same equivalence relation. The way of defining \underline{↔}_{b} on open process expressions employed here is a mild variation of the way weak equivalence was defined in Milner [6]. It does not carry over to full CCS.

Proposition 2 \underline{↔}_{b} ⊆ E × E is a bisimulation and an equivalence, satisfying, for E, F, G ∈ E

E \underline{↔}_{b} F ⇒ E\{G/X\}\underline{↔}_{b} F \{G/X\}.

Proof: The identity relation Id_{E} is a branching bisimulation and if R and S are branching bisimulations, then so are R^{−1} and R ∘ S = {(E, F) | ∃G ∈ E with (E, G) ∈ R and (G, F) ∈ S}. Hence \underline{↔}_{b} is an equivalence.

If R_{i} (i ∈ I) are branching bisimulations, so is ⋃_{i∈I} R_{i}. Thus \underline{↔}_{b} = ⋃\{R | R is a bisimulation\} is a branching bisimulation.

\{(E\{G/X\}, F \{G/X\}) | E \underline{↔}_{b} F, G ∈ E\} ∪ Id_{E} is a bisimulation by Lemma 4 (using =_{α}⊆ \underline{↔}_{b}).□

Proposition 3 If E\{G/X\}\underline{↔}_{b} F \{G/X\} for all closed process expressions G, then E \underline{↔}_{b} F.

Proof: As A is nonempty, there is an a ∈ A. It is easy to see that a^{m} \underline{↮}_{b} a^{n} for m ≠ n, where a^{n} = aa ⋯ a0 with n a’s. Thus, by Proposition 1, for given E and F it is possible to choose n ∈ IN such that a^{n−1} \underline{↮}_{b} H and thus a^{n−1} \underline{↮}_{b} H\{a^{n}/X\} for H ∈ E_{E} ∪ E_{F}. By assumption E\{a^{n}/X\} \underline{↔}_{b} F \{a^{n}/X\}. It suffices to prove that \{(E′, F′) ⊆ E_{E} × E_{F} | E′\{a^{n}/X\} \underline{↔}_{b} F′\{a^{n}/X\}\} is a branching bisimulation, which is a straightforward application of Lemma 4. □

The following is a powerful tool for establishing statements E \underline{↔}_{b} F. It is analogous to Milner’s notions of strong bisimulation up to \underline{↔}_{s} and weak bisimulation up to \underline{↔}_{w}. As for weak bisimulation up to \underline{↔}_{w}, versions of the notion below without the double arrow in the premises are easily seen to be unsound [7].

Definition 9 A branching bisimulation up to \underline{↔}_{b} is a symmetric relation R ⊆ E × E such that if

ERF and E ⟹ E′ ⟶^{x} E′′ with E \underline{↔}_{b} E′ and x ≠ τ ∨ E′ \underline{↮}_{b} E′′ then ∃E′_{1}, E′′_{1}, F′_{1}, F′′_{1}, F′, F′′ such

that

E  R  F
⇓  ⇓
E′ \underline{↔}_{b} E′_{1} R F′_{1} \underline{↔}_{b} F′
↓x  ↓x
E′′ \underline{↔}_{b} E′′_{1} R F′′_{1} \underline{↔}_{b} F′′

Proposition 4 If R is a branching bisimulation up to \underline{↔}_{b} and ERF, then E \underline{↔}_{b} F.

Proof: It suffices to prove that the relation \underline{↔}_{b} R\underline{↔}_{b} = \{(E_{0}, F_{0}) | ∃E, F : E_{0} \underline{↔}_{b} ERF \underline{↔}_{b} F_{0}\} is a branching bisimulation. So suppose E_{0}, E, F and F_{0} are as indicated, and E_{0} ⟶^{x} E′′_{0}. Then either x = τ and E′′_{0} \underline{↔}_{b} E, which completes the proof, or there are E′ and E′′ with E ⟹ E′ ⟶^{x} E′′, E′ \underline{↔}_{b} E_{0} \underline{↔}_{b} E and E′′ \underline{↔}_{b} E′′_{0}(\underline{↮}_{b} E if x = τ). In the latter case apply Definition 9, and use that

F_{0} \underline{↔}_{b} F ⟹ F′ ⟶^{x} F′′ implies x = τ ∧F′′ \underline{↔}_{b} F_{0} or F_{0} ⟹ F′_{0} ⟶^{x} F′′_{0} with F′ \underline{↔}_{b} F′_{0} and F′′ \underline{↔}_{b} F′′_{0}

by Definition 8 (and in one case Lemma 5 to find F′_{0}). □

Just like weak bisimulation equivalence, branching equivalence is not a congruence on BCCS^{ω}. Also the simplest counterexample is the same: a \underline{↔}_{b} τa but, for b ≠ a, a + b\underline{↮}_{b} τa + b. Here, as usual, a0 is abbreviated by a and action prefixing binds stronger than choice. Milner selected weak bisimulation congruence to be the largest (= coarsest) congruence contained in weak equivalence, and the same solution is applied here. Just like weak congruence, branching congruence has a nice characterization, showing that it is close to the original equivalence.

Definition 10 Two expressions E and F are rooted branching bisimulation equivalent or branching (bisimulation) congruent—notation E \underline{↔}_{rb} F —if ∀x ∈ A_{τ} ∪ V:

E ⟶^{x} E′ implies ∃F′ : F ⟶^{x} F′ ∧ E′ \underline{↔}_{b} F′

F ⟶^{x} F′ implies ∃E′ : E ⟶^{x} E′ ∧ E′ \underline{↔}_{b} F′.

Proposition 5 (Congruence) \underline{↔}_{rb} is an equivalence relation such that

if E = F then aE = aF, E + G = F + G, G + E = G + F and μXE = μXF.

Moreover it is the coarsest relation with these properties contained in \underline{↔}_{b}.

Proof: Similar to the congruence proofs for strong and weak bisimulation congruence in [7]. □

The following shows that the definition of \underline{↔}_{rb} for open expressions yields the same notion as the standard approach based on substitution of closed terms.

Proposition 6 Let E, F ∈ E. Then E \underline{↔}_{b} F implies E\{G/X\} \underline{↔}_{b} F \{G/X\} for G ∈ E, and if E\{G/X\}\underline{↔}_{b} F \{G/X\} for closed G ∈ E, then E \underline{↔}_{b} F.

Proof: Straightforward with Lemma 4, using Propositions 2 and 3 and the same G as before. □

Milner [7] listed two results that show how close weak equivalence and congruence are to each other. The first was that for stable processes (processes without outgoing τ-transitions) the equivalence and congruence coincide. This result carries over to branching bisimulation, as follows immediately from the definitions. The second result says that in each weak bisimulation equivalence class there are at most two congruence classes, with representatives E and τE for some E ∈ E. This is not true for branching bisimulation, indicating that branching equivalence and congruence are less close than weak equivalence and congruence. However, a corollary of this property does hold, showing that the distance is still reasonable.

Proposition 7 E \underline{↔}_{b} F ⇔ τE \underline{↔}_{rb} τF. Proof: Immediate from Definition 10. □

This proposition effectively turns any complete axiomatization for \underline{↔}_{rb} into one for \underline{↔}_{b}.

4 The axioms

The following set of axioms will be proven to be sound and complete for \underline{↔}_{rb}. The entries below are actually axiom schemes, in metavariables E, F, G ∈ E, X ∈ V and (in the axiom B) a ∈ A_{τ}. This means that there is an axiom for every choice of E, F, G, X and a. The axiom schemes E1-3 and A1-4 could be replaced by single axioms, by using real variables X, Y and Z instead of the metavariables E, F and G, and adding the law of substitution: if E = F then E{G/X} = F {G/X}, which is sound by Proposition 6. However, this would not work for R1-6, since the bound variable X is allowed to occur in E, F and G. The axioms μXE = μY (E{Y/X}) (α-conversion) are derivable from R1-6, using Theorem 3 and R2.

E1 E = E
E2 if E = F then F = E
E3 if E = F and F = G then E = G
E4 if E = F then aE = aF, E + G = F + G, G + E = G + F, and μXE = μXF
A0 E + 0 = E
A1 E + F = F + E
A2 E + (F + G) = (E + F) + G
A3 E + E = E
B a(τ(E + F) + E) = a(E + F) for a ∈ A_{τ}
R1 μXE = E{μXE/X}
R2 if F = E{F/X} then F = μXE, provided X is guarded in E
R3 μX(X + E) = μXE
R4 μX(τ(τE + F) + G) = μX(τ(E + F) + G), provided X is unguarded in E
R5 μX(τ(X + E) + τ(X + F) + G) = μX(τ(X + E + F) + G)
R6 μX(τ(X + E) + F) = μX(τ(E + F) + F)

One writes T ⊢ E = F, with T a list of axiom names, if the equation E = F is derivable from the axioms in T. Moreover, in this paper the convention is adopted that the axioms E1-4 and A0-3 are always in T, even if not explicitly listed. In the next 3 sections I will establish the following completeness theorems.

• For E, F ∈ E^{g}: E \underline{↔}_{rb} F ⇔ BR1-2 ⊢ E = F

• For E, F ∈ E^{f}: E \underline{↔}_{rb} F ⇔ B ⊢ E = F

• For E, F ∈ E: E \underline{↔}_{rb} F ⇔ BR ⊢ E = F

The rest of this section will be devoted to the soundness of the axioms.

Soundness: The soundness of E1-4 is established in Proposition 5. As far as R1 concerns, one has

μXE ⟶^{x} F ⇔ E\{μXE/X\} ⟶^{x} F from which it follows that μXE \underline{↔}_{rb} E\{μXE/X\} (the terms

are even strongly bisimilar). In the same way the soundness of A0-4 is established. By inspection of their outgoing transitions, it follows that {(τ(E + F) + E, E + F)} ∪ Id_{E} is a branching bisimulation and hence a(τ(E + F) + E)\underline{↔}_{rb} a(E + F).

Proposition 8 If F \underline{↔}_{rb} E\{F/X\} then F \underline{↔}_{rb} μXE, provided X is guarded in E.

Proof: For G, H ∈ E write H(G) for H{G/X}. Let E, F, G ∈ E, such that X is guarded in E, F \underline{↔}_{rb} E(F) and G \underline{↔}_{rb} E(G). I will show that the symmetric closure of \{(H(E(F)), H(E(G))) | H ∈ E\} is a bisimulation up to \underline{↔}_{b}. So suppose that H(E(F)) ⟹ K′ ⟶^{x} K′′ (in this proof one doesn’t even need to assume that H(E(F)) \underline{↔}_{b} K′ and x ≠ τ ∨ K′ \underline{↮}_{b} K′′). As X is guarded in E and hence in H(E), it cannot be that H(E) ⟹⟶^{X} 0, by Lemma 3. Thus K′ and K′′ are of the form H′(F) and H′′(F) by Lemma 4.3, and by Lemma 4.2 H(E(G)) ⟹ H′′′(G) ⟶^{x} H′′′′(G) with H′′′ =_{α} H′ and H′′′′ =_{α} H′′. Furthermore, by Proposition 5, H′(E(F)) \underline{↔}_{b} H′(F), H′′′(G) \underline{↔}_{b} H′(E(G)), H′′(E(F)) \underline{↔}_{b} H′′(F) and H′′′′(G) \underline{↔}_{b} H′′(E(G)). The requirement starting with H(E(G)) follows by symmetry, so the relation is a branching bisimulation up to \underline{↔}_{b} and by Proposition 4 H(E(F)) \underline{↔}_{b} H(E(G)) for H ∈ E. Using this, a repeat of the argument above with K′ = H(E(F)) gives H(E(F))\underline{↔}_{rb} H(E(G)), so in particular E(F)\underline{↔}_{rb} E(G), and hence F \underline{↔}_{rb} G. Finally take G = μXE. □ Proposition 9 μX(τ(τE + F) + G) \underline{↔}_{rb} μX(τ(E + F) + G), provided X is unguarded in E. Proof: By Lemma 3 there are E_{0},…, E_{n} such that τE + F ⟶^{τ} E_{0} ⟶^{τ} E_{1} ⟶^{τ} ⋯ E_{n} ⟶^{X} with E_{0} = E and n ∈ IN. Write E′_{−1} for τE + F and E′′_{0} for E + F. Then by Lemma 4

L ⟶^{τ} E′_{−1}{L/X} ⟶^{τ} E′_{0}{L/X} ⟶^{τ} E′_{1}{L/X} ⟶^{τ} ⋯ E′_{n}{L/X} ⟶^{τ} E′_{−1}{L/X}

for certain E′_{i} =_{α} E_{i} (i = 0, ..., n) and

R ⟶^{τ} E′′_{0}{R/X} ⟶^{τ} E′′_{1}{R/X} ⟶^{τ} ⋯ E′′_{n}{R/X} ⟶^{τ} E′′_{0}{R/X}

for certain E′′_{j} =_{α} E_{j} (j = 1, ..., n). Let R ⊆ E × E be the symmetric closure of

{(H{L/X}, H′{R/X}) | H =_{α} H′} ∪ {(E′_{i}{L/X}, E′′_{j}{R/X}) | −1≤i≤n, 0≤j ≤n} Then R is a branching bisimulation and L\underline{↔}_{rb} R by Lemma 4. □ Proposition 10 μX(τ(X + E) + τ(X + F) + G) \underline{↔}_{rb} μX(τ(X + E + F) + G). Proof: The closure under symmetry and α-recursion of {(H{L/X}, H{R/X}) | H ∈ E}∪

{(τ(X + E){L/X}, τ(X + E + F){R/X}) ∪ {(τ(X + F){L/X}, τ(X + E + F){R/X})} is a branching bisimulation. □ In the same way one proves the soundness of R3 and R6. Proposition 11 μX(X + E) \underline{↔}_{rb} μXE. □ Proposition 12 μX(τ(X + E) + F) \underline{↔}_{rb} μX(τ(E + F) + F). □ Corollary 1 (Soundness) For E, F ∈ E: BR ⊢ E = F ⇒ E \underline{↔}_{rb} F.

5 Completeness for guarded process expressions

Let, for S = {E_{1},…, E_{n}}, ∑ S be an abbreviation for E_{1} + ⋯ + E_{n}. This notation is justified by the axioms A0-3.

Lemma 6 For E ∈ E^{g}, R1 ⊢ E = ∑{aE′ | E ⟶^{a} E′} + ∑{W | E ⟶^{W} 0}.

Proof: By induction on the number of recursion operators in E, not counting the ones that occur in a subterm aG. If this number is 0, then E has the form ∑_{i∈I} a_{i}E_{i} + ∑_{j∈J} W_{j} with a_{i} ∈ A_{τ} and W_{j} ∈ V (the so-called head normal form) and the statement holds trivially. Otherwise E has a summand μXF, which can be replaced by F {μXF/X} using R1, yielding E′′. As E is guarded, E′ has less recursion operators that don’t occur in a subterm aG, so by induction

R1 ⊢ E′′ = ∑{aE′ | E′′ ⟶^{a} E′} + ∑{W | E′′ ⟶^{W} 0}. As E′′ ⟶^{x} E′ ⇔ E ⟶^{x} E′ for x ∈ A_{τ} ∪ V,

the statement follows. □

Definition 11 A recursive specification S is a set of equations {X = S_{X} | X ∈ V_{S}} with V_{S} ⊆ V and S_{X} ∈ E for X ∈ V_{S}. E ∈ E T -provably satisfies the recursive specification S in the variable X_{0} ∈ V_{S} if there are expressions E_{X} for X ∈ V_{S} with E = E_{X_{0}}, such that for X ∈ V_{S}

T ⊢ E_{X} = S_{X}{E_{Y} /Y }_{Y ∈V_{S}}.

Definition 12 Let S be a recursive specification. The relations ⟶^{o}⊆ V_{S} × V_{S} and ⟶^{u}⊆ V_{S} × V_{S} are defined by

• X ⟶^{o} Y if Y occurs free in S_{X}

• X ⟶^{u} Y if Y occurs free and unguarded in S_{X}

Now S is called well-founded if ⟶^{o} is well-founded on V_{S}, and guarded if ⟶^{u} is well-founded on V_{S}.

Proposition 13 (Unique solutions) If S is a finite guarded recursive specification and X_{0} ∈ V_{S}, then there is an expression E which R1-provably satisfies S in X_{0}. Moreover if there are two such expressions E and F, then R2 ⊢ E = F.

Proof: In Milner [6]. □

Theorem 1 Let E_{0}, F_{0} ∈ E^{g} with E_{0} \underline{↔}_{rb} F_{0}. Then there is a finite guarded recursive specification S BR1-provably satisfied in the same variable X_{0} ∈ V_{S} by both E_{0} and F_{0}.

Proof: Take a fresh set of variables V_{S} = \{X_{EF} | E ∈ E_{E_{0}}, F ∈ E_{F_{0}}, E \underline{↔}_{b} F \}. X_{0} = X_{E_{0}F_{0}}. Now for X_{EF} ∈ V_{S}, S contains the equation

X_{EF} = ∑\{W | E ⟶^{W} 0 and F ⟶^{W} 0\} + ∑\{aX_{E′F′} | E ⟶^{a} E′, F ⟶^{a} F′ and E′ \underline{↔}_{b} F′\}+

∑\{τX_{E′F} | X_{EF} ≠ X_{0}, E ⟶^{τ} E′ and E′ \underline{↔}_{b} F \} + ∑\{τX_{EF′} | X_{EF} ≠ X_{0}, F ⟶^{τ} F′ and E \underline{↔}_{b} F′\}.

Using that X_{EF} ⟶^{u} X_{E′F′} iff S_{X_{EF}} has a summand τX_{E′F′}, it is easy to show that any infinite

u-path X_{EF} ⟶^{u} X_{E′F′} ⟶^{u} ⋯ implies an infinite τ-path E ⟶^{τ} E′ ⟶^{τ} ⋯ or F ⟶^{τ} F′ ⟶^{τ} ⋯,

which cannot exist by Lemma 2 since E_{0} and F_{0} are guarded. Hence S is a guarded recursive specification. Moreover S is finite by Proposition 1. It remains to be established that E_{0} BR1provably satisfies S in X_{0}. The same statement for F_{0} then follows by symmetry.

For X_{EF} ∈ V_{S}, let H_{EF} be the expression ∑{W | E ⟶^{W} 0 and F ⟶^{W} 0}+

+ ∑\{aE′ | E ⟶^{a} E′, F ⟶^{a} F′ and E′ \underline{↔}_{b} F′\} + ∑\{τE′ | X_{EF} ≠ X_{0}, E ⟶^{τ} E′ and E′ \underline{↔}_{b} F \}

and define the expression G_{EF} by

G_{EF} = \{ \begin{matrix}H_{EF} + τE & if X_{EF} ≠ X_{0} and ∃F′ with F ⟶^{τ} F′ and E \underline{↔}_{b} F′ \\ E & otherwise. \end{matrix}

It follows from Lemma 6 that R1 ⊢ E = E + H_{EF} and hence BR1 ⊢ a(H_{EF} + τE) = aE. Thus

BR1 ⊢ aG_{EF} = aE for a ∈ A_{τ} .  (1)

It suffices to prove that for X_{EF} ∈ V_{S}

BR1 ⊢ G_{EF} = ∑\{W | E ⟶^{W} 0 and F ⟶^{W} 0\} + ∑\{aG_{E′F′} | E ⟶^{a} E′, F ⟶^{a} F′ and E′ \underline{↔}_{b} F′\}+

∑\{τG_{E′F} | X_{EF} ≠ X_{0}, E ⟶^{τ} E′ and E′ \underline{↔}_{b} F \} + ∑\{τG_{EF′} | X_{EF} ≠ X_{0}, F ⟶^{τ} F′ and E \underline{↔}_{b} F′\}.

By (1) this is equivalent to

BR1 ⊢ G_{EF} = H_{EF} + ∑\{τE | X_{EF} ≠ X_{0}, F ⟶^{τ} F′ and E \underline{↔}_{b} F′\}.  (2)

In case X_{EF} ≠ X_{0} and ∃F′ with F ⟶^{τ} F′ and E \underline{↔}_{b} F′, this follows from the definition of G_{EF}. In case X_{EF} ≠ X_{0} and ∄F′ with F ⟶^{τ} F′ and E \underline{↔}_{b} F′, (2) reduces to BR1 ⊢ E = H_{EF}, and by Lemma 6 if suffices to establish, for x ∈ A_{τ} ∪ V, that

if E ⟶^{x} E′ then \begin{matrix}x = τ and E′ \underline{↔}_{b} F \\ or ∃F′ : F ⟶^{x} F′ ∧ E′ \underline{↔}_{b} F′. \end{matrix}

But this follows from E \underline{↔}_{b} F, using that if F ⟶^{τ} F_{1} ⟹ F′′ with F′′ \underline{↔}_{b} E \underline{↔}_{b} F, then E \underline{↔}_{b} F_{1} by Lemma 5, violating the assumptions. Finally, in case X_{EF} = X_{0}, (2) also reduces to BR1 ⊢ E = H_{EF}, and this time I have to establish, for x ∈ A_{τ} ∪ V, that

if E ⟶^{x} E′ then ∃F′ : F ⟶^{x} F′ ∧ E′ \underline{↔}_{b} F′,

which follows immediately from E \underline{↔}_{rb} F. □

Corollary 2 (Completeness) For E, F ∈ E^{g}: E \underline{↔}_{rb} F ⇔ BR1-2 ⊢ E = F.

6 Completeness for finite process expressions

Theorem 2 Let E_{0}, F_{0} ∈ E^{f} with E_{0} \underline{↔}_{rb} F_{0}. Then there is a finite well-founded recursive specification S B-provably satisfied in the same variable X_{0} ∈ V_{S} by both E_{0} and F_{0}.

Proof: The construction of S is exactly as in the proof of Theorem 1. Using that X_{EF} ⟶^{o} X_{E′F′} iff S_{X_{EF}} has a summand aX_{E′F′} with a ∈ A_{τ}, it is easy to show that any infinite o-path X_{EF} ⟶^{o} X_{E′F′} ⟶^{o} ⋯ implies an infinite path E ⟶^{a_{1}} E′ ⟶^{a_{2}} ⋯ or F ⟶^{b_{1}} F′ ⟶^{b_{2}} ⋯, which cannot exist by Lemma 1 since E_{0} and F_{0} are finite. Hence S is a well-founded recursive specification. The proof that S is finite and provably satisfies both E_{0} and F_{0} in X_{0} is exactly as before, except that Lemma 6 is not needed, as recursion-free process expression are already in head normal form and therefore satisfy

⊢ E = ∑{aE′ | E ⟶^{a} E′} + ∑{W | E ⟶^{W} 0}

without using axiom R1. As this was the only call for this axiom in the proof of Theorem 1 it follows that S is B-provably satisfied in X_{0} ∈ V_{S} by both E_{0} and F_{0}. □

Proposition 14 (Unique solutions) If S is a finite well-founded recursive specification and X_{0} ∈ V_{S}, then there is an expression E which provably satisfies S in X_{0}. Moreover if there are two such expressions E and F, then ⊢ E = F.

Proof: By induction on the number of equations in S I find expressions E_{X} for X ∈ V_{S}, such that

⊢ E_{X} = S_{X}{E_{Y} /Y }_{Y ∈V_{S}}

and if there are F_{X} ∈ E for X ∈ V_{S} such that ⊢ F_{X} = S_{X}{F_{Y} /Y }_{Y ∈V_{S}} then ⊢ E_{X} = F_{Y} for X ∈ V_{S}.

If S has only one equation X = S_{X} then X does not occur free in S_{X} by the well-foundedness of ⟶^{o}. Hence S_{X} provably satisfies S, and for any other expression F satisfying S one has ⊢ F = S_{X}.

Now suppose that S has more than one equation. By the well-foundedness of ⟶^{o} there must be a variable Z ∈ V_{S} such that Y ⟶^{o} Z for no Y ∈ V_{S}. Obtain T from S by deleting the equation Z = S_{Z}. By induction there are E_{X} ∈ E for X ∈ V_{T}, such that ⊢ E_{X} = S_{X}{E_{Y} /Y }_{Y ∈V_{T}} and if there are F_{X} ∈ E for X ∈ V_{T} such that ⊢ F_{X} = S_{X}{F_{Y} /Y }_{Y ∈V_{T}} then ⊢ E_{X} = F_{Y} for X ∈ V_{T}. Let E_{Z} = S_{X}{E_{Y} /Y }_{Y ∈V_{T}}. Then, for X ∈ V_{S},

⊢ E_{X} = S_{X}{E_{Y} /Y }_{Y ∈V_{T}} = S_{X}{E_{Y} /Y }_{Y ∈V_{S}}

and if there are F_{X} ∈ E for X ∈ V_{S} such that ⊢ F_{X} = S_{X}{F_{Y} /Y }_{Y ∈V_{S}} then ⊢ E_{X} = F_{Y} for

X ∈ V_{T} and hence ⊢ F_{Z} = S_{Z}{F_{Y} /Y }_{Y ∈V_{S}} = S_{Z}{F_{Y} /Y }_{Y ∈V_{T}} =^{E4} S_{Z}{E_{Y} /Y }_{Y ∈V_{T}} = E_{Z}. □

Corollary 3 (Completeness) For E, F ∈ E^{f}: E \underline{↔}_{rb} F ⇔ B ⊢ E = F.

7 Completeness for all process expressions

Theorem 3 For every E ∈ E there exists a guarded expression E′ with R1,3-6 ⊢ E = E′.

Proof: It suffices to prove this for expressions of the form E = μXF. Following Milner, I prove a stronger result by induction on the depth of nesting of recursions in F, namely

For every F ∈ E, there exists a guarded expression F′ for which

• X is guarded in F′

• No free unguarded occurrence of any variable in F′ lies within a recursion in F′

• R1,3-6 ⊢ μXF = μXF′.

Assume that this property holds for every G whose recursion depth is less than that of F. Then for each recursion μY G in F that lies within no other recursion in F, there must be a guarded expression G′ such that Y is guarded in G′, no free unguarded occurrence of any variable in G′ lies within a recursion in G′, and R1,3-6 ⊢ μY G = μY G′. These conditions ensure that no free unguarded occurrence of any variable in G′{μY G′/Y } lies within a recursion in this expression.

Let F_{1} be the result of simultaneously replacing every such top-level recursion μY G in F by G′{μY G′/Y }. Clearly F_{1} is guarded, R1,3-6 ⊢ F = F_{1}, and no free unguarded occurrence of any variable in F_{1} lies within a recursion in F_{1}. In converting F_{1} to F′ such that R1,3-6 ⊢ μXF_{1} = μXF′, it remains only to remove all free unguarded occurrences of X from F_{1}, knowing that they do not lie within recursions. Here the axioms R3-6 are applied.

First any free unguarded occurrence of X that is not in the scope of a τ prefixing operator can be removed by R3. Next for any free unguarded occurrence of X that is in the scope of 2 or more τ’s, this number can be lowered by application of R4. Applying R4 from left to right does not change the number of free unguarded occurrences of X, and does not raise the number of τ’s scoping any particular such occurrence. So after finitely many applications all free unguarded occurrences of X are in the scope of exactly one τ operator, and applying R5 makes that they are all in the scope of the same τ. Finally by A3 at most one such occurrence remains, and this one is eliminated by R6. □

Corollary 4 For E, F ∈ E: E \underline{↔}_{rb} F ⇔ BR ⊢ E = F.

8 Concluding remarks

The notion of branching bisimulation congruence employed here • equates livelock and deadlock: μX(τX) = τ0

• does not equate divergence and livelock: μX(τX + E) ≠ μX(τX) + E

• abstracts from divergence: μX(τX + τE) = τE

• and chooses minimal solutions in case of underspecification: μXX = 0, just as Milner’s standard version of weak bisimulation congruence. As in the case of weak congruence, there are alternative versions of branching congruence where these choices are made differently [4]. Complete axiomatizations for these notions remain to be provided. For weak bisimulation, such work has been done in Walker [8].

For arbitrary cardinals κ, one could define the language BCCS^{κ} by allowing sets of expressions as argument of a choice operator ∑, and functions V_{S} → E for V_{S} ⊆ V as argument of a recursion operator μ, as long as the size of these sets and functions is less than κ. Such a language would represent all and only the behavious with less than κ states. In generalizing the completeness theorem for guarded BCCS^{κ} expressions, one has to reformulate most axioms in an obvious way to deal with the new operators, slightly adapt the proof of Lemma 6 and make sure that there are at least κ variables in order for the first act in the proof of Theorem 1 to be possible. But nothing in my proof essentially depends on finiteness, and the result generalizes smoothly to guarded infinitestate behaviours. One could even take V to be a proper class and do away with all cardinality restrictions. Of course these axiomatizations are not effective, as some axioms have infinitely many premisis. The case for unguared expressions does not generalize in this way, as not every unguarded BCCS^{κ} expression is branching congruent with a guarded one.

By combining the axioms presented here with the complete axiomatizations for strong bisimulation that allow closed CCS, CSP and ACP expressions to be converted into head normal form, one obtains complete axiomatizations for closed terms in the language BCCS^{ω} to which the ACCSP operators have been added, provided that they do not occur in the scope of recursion operators (cf. Milner [6]). Remarkably, in this setting the axiom B can be simplified to aτX = aX.

Theorem 4 Every closed instance of B is derivable from aτX = aX.

Proof: (sketch) a(bc + cb) + cab = ab∥c = aτb∥c = a(τ(bc + cb) + cτb) + caτb. Placing both sides in CSP’s synchronous composition with a(b+c) yields a(b+c) = a(τ(b+c)+c). In this proof b can be replaced by ∑_{i∈I} b_{i} and similarly for c. Now a parallel composition with a(∑_{i∈I} b_{i}E_{i} + ∑_{j∈J} c_{j}F_{j}), in which synchronization is required (only) for a, b_{i} and c_{j} yields

a(∑_{i∈I} b_{i}E_{i} + ∑_{j∈J} c_{j}F_{j}) = a(τ(∑_{i∈I} b_{i}E_{i} + ∑_{j∈J} c_{j}F_{j}) + ∑_{j∈J} c_{j}F_{j}).

(In fact, one needs to assume here that the b_{i} and c_{j} are pairwise distinct, and do not occur in E_{h} and F_{k}, but this restriction can be removed with a relabelling.) □

If one would now require an abstract congruence to satisfy aτX = aX, and an interleaving congruence to be a congruence for all the operators needed above and to satisfy the equations needed above (which are standard and already satisfied by strong congruence), and if one agrees that any finite process is representable by an expression ∑ a_{i}E_{i}, then it follows that for finite processes branching bisimulation is the finest abstract interleaving congruence that generalizes τ-less bisimulation.

References

[1] J.A. Bergstra & J.W. Klop (1985): Algebra of communicating processes with abstraction. Theoretical Computer Science 37(1), pp. 77–121.

[2] J.A. Bergstra & J.W. Klop (1988): A complete inference system for regular processes with silent moves. In F.R. Drake & J.K. Truss, editors: Proceedings Logic Colloquium 1986, Hull, North-Holland, pp. 21–81. First appeared as: Report CS-R8420, CWI, Amsterdam, 1984.

[3] R.J. van Glabbeek (1990): The linear time – branching time spectrum. In J.C.M. Baeten & J.W. Klop, editors: Proceedings CONCUR 90, Amsterdam, LNCS 458, Springer-Verlag, pp. 278–297.

[4] R.J. van Glabbeek & W.P. Weijland (1990): Branching time and abstraction in bisimulation semantics. Technical Report TUM-I9052, SFB-Bericht Nr. 342/29/90 A, Institut für Informatik, Technische Universität München, Munich, Germany. Extended abstract in G.X. Ritter, editor: Information Processing 89, Proceedings of the IFIP 11th World Computer Congress, San Fransisco, USA 1989, Elsevier Science Publishers B.V. (North-Holland), 1989, pp. 613-618.

[5] R. Milner (1984): A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences 28, pp. 439–466.

[6] R. Milner (1989): A complete axiomatisation for observational congruence of finite-state behaviours. Information and Computation 81, pp. 227–247.

[7] R. Milner (1990): Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor: Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201–1242. Alternatively see Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989, of which an earlier version appeared as A Calculus of Communicating Systems, LNCS 92, Springer-Verlag, 1980.

[8] D.J. Walker (1990): Bisimulation and divergence. Information and Computation 85(2), pp. 202–241.