Rooted Divergence-Preserving Branching Bisimilarity is a Congruence

Rob van Glabbeek

Data61, CSIRO, Sydney, Australia School of Computer Science and Engineering,

University of New South Wales, Sydney, Australia

            rvg@cs.stanford.edu

Bas Luttik & Linda Spaninks

Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands

                                                           s.p.luttik@tue.nl

Abstract We prove that rooted divergence-preserving branching bisimilarity is a congruence for the process specification language consisting of 0, action prefix, choice, and the recursion construct μX. .

Keywords: Process algebra; Recursion; Branching bisimulation; Divergence; Congruence.

1 Introduction

Branching bisimilarity [13] is a behavioural equivalence on processes that is compatible with abstraction from internal activity, while at the same time preserving the branching structure of processes in a strong sense [9]. Branching bisimilarity abstracts to a large extent from divergence (i.e., infinite internal activity). For instance, it identifies a process, say P, that may perform some internal activity after which it returns to its initial state (i.e., P has a τ-loop) with a process, say P′, that admits the same behaviour as P except that it cannot perform the internal activity leading to the initial state (i.e., P′ is P without the τ-loop).

In situations where fairness principles apply, abstraction from divergence is often desirable. But there are circumstances in which abstraction from divergence is undesirable: A behavioural equivalence that abstracts from divergence is not compatible with any temporal logic featuring an eventually modality: for any desired state that P′ will eventually reach, the mentioned internal activity of P may be performed forever, and thus prevent P from reaching this desired state. It is also generally not compatible with a process-algebraic priority operator (cf. [23, pp. 130–132]) or sequencing operator [3]. Since a divergence may be exploited to simulate recursively enumerable branching in a computable transition system [21], a divergence-insensitive behavioural equivalence may be considered too coarse for a theory that integrates computability and concurrency [2]. Preservation of divergence is widely considered an important correctness criterion when studying the relative expressiveness of process calculi [14, 25, 6].

The notion of branching bisimilarity with explicit divergence, also stemming from [13], is a suitable refinement of branching bisimilarity that is compatible with the well-known branching-time temporal logic CTL^{∗} without the nexttime operator X (which is known to be incompatible with abstraction from internal activity). In fact, in [12] we have proved that it is the coarsest semantic equivalence on labelled transition systems with silent moves that is a congruence for parallel composition (as found in process algebras like CCS, CSP or ACP) and only equates processes satisfying the same CTL_{−X}^{∗} formulas. In [2], for stylistic reasons, branching bisimilarity with explicit divergence was named divergence-preserving branching bisimilarity; we shall henceforth use this term.

Divergence-preserving branching bisimilarity is the finest behavioural equivalence in the linear time — branching time spectrum [8]. It is the principal behavioural equivalence underlying the theory of executability [1, 2, 16, 17]. Reduction modulo divergence-preserving branching bisimilarity is a part of methods for formal verification and analysis of the behaviour of systems [18, 24, 22, 26]. In [5] a game-based characterisation of divergence-preserving branching bisimilarity is presented.

Processes are usually specified in some process specification language. For compositional reasoning it is then important that the behavioural equivalence used is a congruence with respect to the constructs of that language. Following Milner [19], we consider the language basic CCS with recursion, i.e., the language consisting of 0, action prefix, and choice, extended with the recursion construct μX. ; this language precisely allows the specification of finite-state behaviours. It is easy to see that divergence-preserving branching bisimilarity is not a congruence for that language; in fact, it is not a congruence for any language that includes choice. The goal of this paper is to prove that adding the usual root condition suffices to obtain a congruence—and, in fact, the coarsest congruence—for the language under consideration that is included in divergencepreserving branching bisimilarity.

Recently, a congruence format was proposed for (rooted) divergence-preserving branching bisimilarity [4]. The operational rules for action prefix and choice are in this format. Unfortunately, however, this format does not support the recursion construct μX. . Interestingly, as far as we know, the recursion construct has not been covered at all in the rich literature on congruence formats, with the recent exception of [10]. (The article [10] differentiates between lean and full congruences for recursion; in this article we consider the full congruence.)

The congruence result obtained in this paper should serve as a stepping stone towards a complete axiomatisation of divergence-preserving branching bisimilarity for basic CCS with recursion. Such work, inspired by Milner’s complete axiomatisation of weak bisimilarity [19], would combine the adaptations of [7] to branching bisimilarity, and of [15] to several divergence-sensitive variants of weak bisimilarity.

2 Rooted divergence-preserving branching bisimilarity

Let A be a non-empty set of actions, and let τ be a special action not in A. Let A_{τ} = A ∪ {τ}. Furthermore, let V be a set of recursion variables. The set of process expressions E is generated by the following grammar:

E ::= 0 | X | α.E | μX.E | E + E (α ∈ A_{τ} , X ∈ V) .

An occurrence of a recursion variable X in a process expression E is bound if it is in de scope of a μX. , and otherwise it is free. We denote by FV (E) the set of variables with a free occurrence in E. If X⃗ = X_{0}, …, X_{n} is a sequence of variables, and F⃗ = F_{0}, …, F_{n} is a sequence of process expressions of the same length, then we write E[F⃗/X⃗] for the process expression obtained from E by replacing all free occurrences of X_{i} in E by F_{i} (i = 0, …, n), applying α-conversion to E if necessary to avoid capture.

On E we define an A_{τ} -labelled transition relation ⟶ ⊆ E ×A_{τ} ×E as the least ternary relation satisfying the following rules for all α ∈ A_{τ}, X ∈ V, and process expressions E, E′, F and F′:

1 \overline{α.E ⟶^{α} E}  2 \frac{E[μX.E/X] ⟶^{α} E′}{μX.E ⟶^{α} E′}  3 \begin{matrix}E & ⟶^{α} & E & ′ \\ E & + & F & ⟶^{α} & E & ′ \end{matrix}  4 \begin{matrix}F & ⟶^{α} & F & ′ \\ E & + & F & ⟶^{α} & F & ′ \end{matrix}

We write E ⟶^{α} E′ for (E, α, E′) ∈ ⟶ and we abbreviate the statement ‘E ⟶^{α} E′ or (α = τ and E = E′)’ by E ⟶^{(α)} E′. Furthermore, we write −↠ for the reflexive-transitive closure of ⟶^{τ},

i.e., E −↠ E′ if there exist E_{0}, E_{1}, …, E_{n} ∈ E such that E = E_{0} ⟶^{τ} E_{1} ⟶^{τ} ⋯ ⟶^{τ} E_{n} = E′.

A process expression is closed if it contains no free occurrences of recursion variables; we denote by P the subset of E consisting of all closed process expressions. It is easy to check that if P is a closed process expression and P ⟶^{α} E, then E is a closed process expression too. Hence, the transition relation restricts in a natural way to closed process expressions, and thus associates with every closed process expression a behaviour. We proceed to define when two process expressions may be considered to represent the same behaviour.

Definition 1. A symmetric binary relation R on P is a branching bisimulation if it satisfies the following condition for all P, Q ∈ P and α ∈ A_{τ}:

(T) if P R Q and P ⟶^{α} P′ for some closed process expression P′, then there exist closed process

expressions Q′ and Q′′ such that Q −↠ Q′′ ⟶^{(α)} Q′, P R Q′′ and P′ R Q′.

We write P \underline{↔}_{b} Q if there exists a branching bisimulation R such that P R Q. The relation \underline{↔}_{b} is referred to as branching bisimilarity.

We say that a branching bisimulation R preserves (internal) divergence if

(D) if P R Q and there is an infinite sequence of closed process expressions (P_{k})_{k∈ω} such that P = P_{0}, P_{k} ⟶^{τ} P_{k+1} and P_{k} R Q for all k ∈ ω, then there is an infinite sequence of closed process expressions (Q_{ℓ})_{ℓ∈ω} such that Q = Q_{0}, Q_{ℓ} ⟶^{τ} Q_{ℓ+1} and P_{k} R Q_{ℓ} for all k, ℓ ∈ ω.

We write P \underline{↔}_{b}^{Δ} Q if there exists a divergence-preserving branching bisimulation R such that P R Q. The relation \underline{↔}_{b}^{Δ} was introduced in [13] under the name branching bisimilarity with explicit divergence and is here referred to as divergence-preserving branching bisimilarity.

The relation \underline{↔}_{b}^{Δ} was studied in detail in [11]; we recap some of the facts established ibidem. First, the relation \underline{↔}_{b}^{Δ} is an equivalence relation. Second, the relation \underline{↔}_{b}^{Δ} satisfies the condi-

tion (T), with the following generalisation as a straightforward consequence.

Lemma 2. Let P and Q be closed process expressions. If P \underline{↔}_{b}^{Δ} Q and P −↠ P′′ ⟶^{α} P′ for some closed process expressions P′ and P′′, then there exist closed process expressions Q′ and Q′′ such

that Q −↠ Q′′ ⟶^{α} Q′, P′′ \underline{↔}_{b}^{Δ} Q′′ and P′ \underline{↔}_{b}^{Δ} Q′.

Third, \underline{↔}_{b}^{Δ} also satisfies (D). In [11] several alternative definitions of divergence preservation are studied, which, in the end, all give rise to the same notion of divergence-preserving branching bisimilarity. In particular, the following alternative relational characterisations will be useful tools in the remainder.

Proposition 3. Let P and Q be closed process expressions. Then

• P \underline{↔}_{b}^{Δ} Q if, and only if, P and Q are related by some branching bisimulation R satisfying

(D′) if P R Q and there is an infinite sequence of closed process expressions (P_{k})_{k∈ω} such that P = P_{0} and P_{k} ⟶^{τ} P_{k+1}, then there is an infinite sequence of closed process expressions (Q_{ℓ})_{ℓ∈ω} and a mapping σ : ω → ω such that Q = Q_{0}, Q_{ℓ} ⟶^{τ} Q_{ℓ+1} and P_{σ(ℓ)} R Q_{ℓ} for all ℓ ∈ ω; and

• P \underline{↔}_{b}^{Δ} Q if, and only if, P and Q are related by some branching bisimulation R satisfying

(D′′) if P R Q and there is an infinite sequence of closed process expressions (P_{k})_{k∈ω} such that P = P_{0} and P_{k} ⟶^{τ} P_{k+1}, then there exists a closed process expression Q′ such that Q ⟶^{τ} Q′ and P_{k} R Q′ for some k ∈ ω.

Moreover, \underline{↔}_{b}^{Δ} itself satisfies (D′) and (D′′).

Proof. See [11]; condition (D′) is (D3) and condition (D′′) is (D2).

And finally, it was proved in [11] that \underline{↔}_{b}^{Δ} satisfies the following so-called stuttering property.

Proposition 4. Let P be a closed process expression and let Q_{0}, …, Q_{k} be closed process expressions such that Q_{0} ⟶^{τ} ⋯ ⟶^{τ} Q_{k}. If P \underline{↔}_{b}^{Δ} Q_{0} and P \underline{↔}_{b}^{Δ} Q_{k}, then P \underline{↔}_{b}^{Δ} Q_{i} for all 0 ≤ i ≤ k.

The relation \underline{↔}_{b}^{Δ} is not compatible with + (0 \underline{↔}_{b}^{Δ} τ.0 but 0 + a.0 \underline{↮}_{b}^{Δ} τ.0 + a.0), and hence not a congruence for the language we are considering. We proceed to define a relation for which we shall prove that it is the coarsest congruence for our language that is contained in \underline{↔}_{b}^{Δ}.

Definition 5. Let P and Q be closed process expressions. We say that P and Q are rooted divergence-preserving branching bisimilar (notation: P \underline{↔}_{rb}^{Δ} Q) if for all α ∈ A_{τ} the following holds:

(R1) if P ⟶^{α} P′, then there exists a Q′ such that Q ⟶^{α} Q′ and P′ \underline{↔}_{b}^{Δ} Q′; and

(R2) if Q ⟶^{α} Q′, then there exists a P′ such that P ⟶^{α} P′ and P′ \underline{↔}_{b}^{Δ} Q′.

The following proposition is a straightforward consequence of the fact that \underline{↔}_{b}^{Δ} is an equivalence.

Proposition 6. The relation \underline{↔}_{rb}^{Δ} is an equivalence relation on P.

Moreover, it is easy to verify that \underline{↔}_{rb}^{Δ} ⊆ \underline{↔}_{b}^{Δ}.

We have defined the notions of \underline{↔}_{b}^{Δ} and \underline{↔}_{rb}^{Δ} on closed process expressions because those are thought of as directly representing behaviour. Due to the presence of the binding construct μX. it is, however, convenient to lift these notions to expressions with free variables even if the goal is simply to establish behavioural equivalence of closed process expressions.

Definition 7. Let E and F be process expressions, and let the sequence X⃗ of variables at least include all the variables with a free occurrence in E or F. We write E \underline{↔}_{rb}^{Δ} F (E \underline{↔}_{b}^{Δ} F) if E[P⃗/X⃗] \underline{↔}_{rb}^{Δ} F[P⃗/X⃗] (E[P⃗/X⃗] \underline{↔}_{b}^{Δ} F[P⃗/X⃗]) for every sequence of closed process expressions P⃗ of the same length as X⃗.

It is clear from the definition above that, since \underline{↔}_{rb}^{Δ} is an equivalence relation on P, its lifted version is an equivalence relation on E. We shall prove that it is also compatible with the constructs of the syntax, i.e., if E \underline{↔}_{rb}^{Δ} F, then α.E \underline{↔}_{rb}^{Δ} α.F for all α ∈ A_{τ}, μX.E \underline{↔}_{rb}^{Δ} μX.F for all X ∈ V, E + H \underline{↔}_{rb}^{Δ} F + H and H + E \underline{↔}_{rb}^{Δ} H + F for all process expressions H. To prove that \underline{↔}_{rb}^{Δ} is compatible with α. and + is straightforward, but for μX. this is considerably more work.

3 The congruence proof

Our proof that \underline{↔}_{rb}^{Δ} is compatible with μX. relies on the following observation: If Y⃗ is some sequence of variables and P⃗ is a sequence of closed terms of the same length, then, on the one hand, E \underline{↔}_{rb} F implies E[P⃗/Y⃗] \underline{↔}_{rb}^{Δ} F[P⃗/Y⃗], and, on the other hand, if X does not occur in Y⃗, then from μX.E[P⃗/Y⃗] \underline{↔}_{rb}^{Δ} μX.F[P⃗/Y⃗] it follows that (μX.E)[P⃗/Y⃗] \underline{↔}_{rb}^{Δ} (μX.F)[P⃗/Y⃗]. Therefore, it is enough to establish that E \underline{↔}_{rb}^{Δ} F implies μX.E \underline{↔}_{rb}^{Δ} μX.F in the special case that E and F are process expressions with no other free variables than X; such process expressions will be called X-closed.

The rest of this section is organised as follows.

We shall first characterise, in Section 3.1, the relation \underline{↔}_{rb}^{Δ} on X-closed process expressions in terms of the transition relation on X-closed process expressions.

Then, in Section 3.2, we shall present a suitable notion of rooted divergence-preserving branching bisimulation up to \underline{↔}_{rb}^{Δ}, and we shall prove that every pair of rooted divergence-preserving branching bisimilar X-closed process expressions (E, F) gives rise to a relation R^{u} of which we can show that it is a rooted divergence-preserving branching bisimulation up to \underline{↔}_{rb}^{Δ}. The relation R^{u} will be defined in such a way that it relates μX.E and μX.F and thus allows us to conclude that these process expressions are rooted divergence-preserving bisimilar.

In Section 3.3, we shall then put the pieces together and prove \underline{↔}_{rb}^{Δ} is the coarsest congruence contained in \underline{↔}_{b}^{Δ} for basic CCS with recursion.

3.1 \underline{↔}_{b}^{Δ} on X-closed process expressions

We say that a process expression E is X-closed if FV (E) ⊆ {X}; the set of all X-closed process expressions is denoted by P_{X}. Note that if E is X-closed and E ⟶^{α} E′, then E′ is X-closed too, and so the A_{τ} -labelled transition relation restricts in a natural way to X-closed process expressions.

Definition 8. We define when X is exposed in a (not necessarily X-closed) process expression E with induction on the structure of E:

i. if E = X, then X is exposed in E;

ii. if E = μY.E′, Y is a recursion variable distinct from X and X is exposed in E′, then X is exposed in E;

iii. if E = E_{1} + E_{2} and X is exposed in E_{1} or E_{2}, then X is exposed in E.

Note that the variable X is exposed in E if, and only if, E has an unguarded occurrence of X in the sense of [19].

We establish a relationship between the transitions of a closed process expression E[P/X] that is obtained by substituting a closed process expression P for the variable X in an X-closed process expression E, and the transitions of E and P.

Lemma 9. Let E be an X-closed process expression, and let P be a closed process expression.

1. If E ⟶^{α} E′, then E[P/X] ⟶^{α} E′[P/X], and if X is exposed in E and P ⟶^{α} P′, then

E[P/X] ⟶^{α} P′.

2. If E[P/X] ⟶^{α} P′ for some closed process expression P′, then either there exists an X-closed process expression E′ such that E ⟶^{α} E′ and P′ = E′[P/X], or X is exposed in E, P ⟶^{α} P′ and every derivation of E[P/X] ⟶^{α} P′ has a derivation of P ⟶^{α} P′ as a subderivation.

Proof. Statement 1 of the lemma is established with straightforward inductions on a derivation of E ⟶^{α} E′ and on the structure of E.

We proceed to establish with induction on a derivation of E[P/X] ⟶^{α} P′ that there exists an X-closed process expression E′ such that E ⟶^{α} E′ and P′ = E′[P/X], or X is exposed in E, P ⟶^{α} P′ and a derivation of P ⟶^{α} P′ appears as a subderivation of the considered derivation of E[P/X] ⟶^{α} P′. This implies statement 2.

We distinguish cases according to the structure of E:

• Clearly, E cannot be 0, for if E = 0, then E[P/X] = 0, and 0 does not admit any transitions.

• If E = X, then X is exposed in E and P = E[P/X] ⟶^{α} P′. It is then also immediate that the considered derivation of E[P/X] ⟶^{α} P′ has a derivation of P ⟶^{α} P′ as a subderivation.

• If E = β.E′ for some β ∈ A_{τ} and some X-closed process expression E′, then β = α and E ⟶^{β} E′. Since E[P/X] = β.(E′[P/X]), rule 1 is the last rule applied in the derivation of the transition E[P/X] ⟶^{α} P′, so P′ = E′[P/X].

• If E = μY.F for some process expression F with FV (F) ⊆ {X, Y}, then there are two subcases:

On the one hand, if Y = X, then, since X has no free occurrence in E, we have E = E[P/X] ⟶^{α} P′. Furthermore, since P′ is closed we have that P′ = P′[P/X].

On the other hand, if Y ≠ X, then E[P/X] = μY.(F[P/X]), and therefore the last rule applied in the considered derivation of the transition E[P/X] ⟶^{α} P′ is rule 2. Consequently, the considered derivation has a proper subderivation of the transition F[P/X][μY.(F[P/X])/Y] ⟶^{α} P′. Note that F[P/X][μY.(F[P/X])/Y] = (F[μY.F/Y])[P/X]. Hence, by the induction hypothesis, either there exists an E′ such that F[μY.F/Y] ⟶^{α} E′ and P′ = E′[P/X], or X is exposed in F[μY.F/Y], P ⟶^{α} P′, and the derivation of F[μY.F/Y][P/X] ⟶^{α} P′ has a derivation of P ⟶^{α} P′ as a subderivation. In the first case, it follows from F[μY.F/Y] ⟶^{α} E′, by rule 2, that E = μY.F ⟶^{α} E′ and P′ = E′[P/X]. In the second case, it suffices to note that X is exposed in F, hence also in E, and that a derivation of P ⟶^{α} P′ appears as a subderivation of the considered derivation of E[P/X] ⟶^{α} P′.

• If E = E_{1} + E_{2}, then [E][P/X] = E_{1}[P/X] + E_{2}[P/X].

The last rule applied in the considered derivation of the transition [E][P/X] ⟶^{α} P′ is either rule 3 or rule 4.

If it is rule 3, then E_{1}[P/X] ⟶^{α} P′, and since this transition has a derivation that is a proper subderivation of the considered derivation of [E][P/X] ⟶^{α} P′, by the induction hypothesis it follows that either E_{1} ⟶^{α} E′ and P′ = E′[P/X], or X is exposed in E_{1}, P ⟶^{α} P′, and a derivation of P ⟶^{α} P′ appears as a subderivation the derivation of E_{1}[P/X] ⟶^{α} P′.

In the first case, it remains to note that then also E ⟶^{α} E′, and in the second case, it remains to note that X is also exposed in E.

If the last rule applied in the considered derivation is rule 4, then the proof is analogous.

Corollary 10. Let E be an X-closed process expression. If E[μX.E/X] ⟶^{α} P′ for some closed process expression P′, then there exists an X-closed process expression E′ such that E ⟶^{α} E′ and P′ = E′[μX.E/X].

Proof. Consider a derivation of E[μX.E/X] ⟶^{α} P′ that is minimal in the sense that it does not have a derivation of E[μX.E/X] ⟶^{α} P′ as proper subderivation. Let P = μX.E. Since every derivation of P ⟶^{α} P′ has a derivation of E[P/X] ⟶^{a} P′ as a proper subderivation (see the operational rules, and rule 2 in particular), it follows that the considered derivation of E[μX.E/X] ⟶^{α} P′ does not have a subderivation of P ⟶^{α} P′. Hence, by Lemma 9.2 there exists an X-closed process expression E′ such that E ⟶^{α} E′ and P′ = E′[μX.E/X].

Corollary 11. Let G_{0} and E be X-closed process expressions. If there is an infinite sequence of closed process expressions (P_{k})_{k∈ω} such that G_{0}[μX.E/X]=P_{0} and P_{k} ⟶^{τ} P_{k+1} for all k ∈ ω, then there is an infinite sequence of X-closed process expressions (G_{k})_{k∈ω} such that P_{k} = G_{k}[μX.E/X] and, for all k ∈ ω, either G_{k} ⟶^{τ} G_{k+1} or X is exposed in G_{k} and E ⟶^{τ} G_{k+1}.

Proof. We construct (G_{k})_{k∈ω} with induction on k. Suppose that G_{k} with G_{k}[μX.E/X] = P_{k} has already been constructed. Since P_{k} ⟶^{τ} P_{k+1}, by Lemma 9.2 there are two cases: either there is a G_{k+1} with G_{k} ⟶^{τ} G_{k+1} and P_{k+1} = G_{k+1}[μX.E/X], in which case we are done, or X is exposed in G_{k} and μX.E ⟶^{τ} P_{k+1}. In the latter case E[μX.E/X] ⟶^{τ} P_{k+1} (see the operational rules, and rule 2 in particular). By Corollary 10 there exists an X-closed process expression G_{k+1} such

that E ⟶^{τ} G_{k+1} and P_{k+1} = G_{k+1}[μX.E/X].

Let E and E′ be process expressions. We write E ⟶ E′ if there exists an α ∈ A_{τ} such that E ⟶^{α} E′, and denote by ⟶^{∗} the reflexive-transitive closure of ⟶. If E ⟶^{∗} E′, then we say that E′ is reachable from E.

Proposition 12 ([7, Proposition 1]). If E is a process expression, then the set of all expressions reachable from E is finite.

On E we define an V ⊎ A_{τ} -labelled transition relation ⟶ ⊆ E × (V ⊎ A_{τ}) × E as the least ternary relation satisfying, besides the four rules of Section 2, also the rule

5 \overline{X ⟶^{X} 0}

for each X ∈ V. Intuitively, the V ⊎A_{τ} -labelled transition relation treats a process expression E as the closed term obtained from E by replacing all free occurrences of the variable X by the closed process expression X.0 in which X is interpreted as an action instead of as a recursion variable. Note that a variable X is exposed in an expression E according to Definition 8 iff ∃F. E ⟶^{X} F, which is the case iff E ⟶^{X} 0. Now let \underline{↔}_{bX}^{Δ} and \underline{↔}_{rbX}^{Δ} be defined exactly like \underline{↔}_{b}^{Δ} and \underline{↔}_{rb}^{Δ}, but using the V ⊎ A_{τ} -labelled transition relation instead of the A_{τ} -labelled one, and applying all definitions directly to expressions with free variables, instead of applying the lifting of Definition 7.

We proceed to show that on X-closed process expressions \underline{↔}_{bX}^{Δ} coincides with \underline{↔}_{b}^{Δ}, and \underline{↔}_{rbX}^{Δ} with \underline{↔}_{rb}^{Δ}. This characterisation, for weak and branching bisimilarity without preservation of divergence, stems from [19] and [7]. Here we use it solely to obtain Corollaries 15 and 16.

Lemma 13. The relation

B = \{(E[P/X], F[P/X]) | E, F are X-closed, E \underline{↔}_{bX}^{Δ} F, P is closed\}

is a branching bisimulation satisfying (D′′) of Proposition 3.

Proof. It is immediate from its definition that B is symmetric.

We show it satisfies (T). Suppose E, F are X-closed, E \underline{↔}_{bX}^{Δ} F and P closed. Let E[P/X] ⟶^{α} P′ for some α ∈ A_{τ}. By Lemma 9.2 either there exists an X-closed process expression E′ such that E ⟶^{α} E′ and P′ = E′[P/X], or X is exposed in E and P ⟶^{α} P′. In the first case, since E \underline{↔}_{bX}^{Δ} F, there exist process expressions F′ and F′′ such that F −↠ F′′ ⟶^{(α)} F′, E \underline{↔}_{bX}^{Δ} F′′ and

E′ \underline{↔}_{bX}^{Δ} F′. By Lemma 9.1 F[P/X] −↠ F′′[P/X] ⟶^{(α)} F′[P/X]. Furthermore, E[P/X] B F′′[P/X]

and P′ = E′[P/X] B F′[P/X]. In the second case, since X is exposed in E, we have that E ⟶^{X} 0 and hence, since E \underline{↔}_{bX}^{Δ} F, there exist process expressions F′ and F′′ such that F −↠ F′′ ⟶^{X} F′, E \underline{↔}_{bX}^{Δ} F′′ and 0 \underline{↔}_{bX}^{Δ} F′. Moreover, since F′′ ⟶^{X} F′, X is exposed in F′′, so by Lemma 9.1

F[P/X] −↠ F′′[P/X] ⟶^{α} P′. Furthermore, E[P/X] B F′′[P/X] and P′ B P′.

It remains to show that B satisfies (D′′). Suppose E, F are X-closed, E \underline{↔}_{bX}^{Δ} F and P is closed, and there is an infinite sequence of closed process expressions (P_{k})_{k∈ω} such that E[P/X] = P_{0} and P_{k} ⟶^{τ} P_{k+1}. By Lemma 9.2 either there exists an infinite sequence of X-closed process expressions (E_{k})_{k∈ω} such that E_{0} = E, E_{k} ⟶^{τ} E_{k+1} and P_{k+1} = E_{k+1}[P/X] for all k ∈ ω, or there exists a finite sequence of X-closed process expressions (E_{i})_{i≤k} for some k ∈ ω such that E_{0} = E,

E_{i} ⟶^{τ} E_{i+1} and P_{i+1} = E_{i+1}[P/X] for all i < k, E_{k} ⟶^{X} 0 and P ⟶^{τ} P_{k+1}. In the first case,

since E \underline{↔}_{bX}^{Δ} F, using (D′′), there exist a process expression F′ such that F ⟶^{τ} F′ and E_{k} \underline{↔}_{bX}^{Δ} F′ for some k ∈ N. By Lemma 9.1 F[P/X] ⟶^{τ} F′[P/X]. Furthermore, E_{k}[P/X] B F′[P/X]. In the second case, since E \underline{↔}_{bX}^{Δ} F, with induction on i there exists a sequence F_{0}, …, F_{m}, F_{m+1} and a

mapping ρ : {0, …, m} → {0, …, k} with ρ(m) = k such that F = F_{0} ⟶^{τ} ⋯ ⟶^{τ} F_{m} ⟶^{X} F_{m+1}

and E_{ρ(j)} \underline{↔}_{b}^{Δ} F_{j} for all j = 0, …, m. If m = 0, then X is exposed in F, so by Lemma 9.1 F[P/X] ⟶^{τ} P_{k+1}. Furthermore, P_{k+1} B P_{k+1}. If m > 0, then let F′ = F_{1}. By Lemma 9.1

F[P/X] ⟶^{τ} F′[P/X]. Furthermore, E_{ρ(1)}[P/X] B F′[P/X].

For every α ∈ A_{τ} and n ∈ ω, we define the closed process expression α^{n} inductively by α^{0} = 0 and α^{n+1} = α.α^{n}. Note that, if α ≠ τ, then α^{i} \underline{↔}_{b}^{Δ} α^{j} implies i = j. Recall that we have assumed that A is non-empty; we now fix, for the remainder of this section, a particular action a ∈ A.

Proposition 14. Let E and F be X-closed process expressions. Then E \underline{↔}_{bX}^{Δ} F iff E \underline{↔}_{b}^{Δ} F, and E \underline{↔}_{rbX}^{Δ} F iff E \underline{↔}_{rb}^{Δ} F.

Proof. We need to show that E \underline{↔}_{bX}^{Δ} F iff E[P/X] \underline{↔}_{b}^{Δ} F[P/X] for each closed process expression P, and likewise E \underline{↔}_{rbX}^{Δ} F iff E[P/X] \underline{↔}_{rb}^{Δ} F[P/X] for each closed process expression P.

“Only if”: Lemma 13 immediately yields that E \underline{↔}_{bX}^{Δ} F implies E[P/X] \underline{↔}_{b}^{Δ} F[P/X] for each closed process expression P. Now let E \underline{↔}_{rbX}^{Δ} F and E[P/X] ⟶^{α} P′. By Lemma 9.2 either there exists an X-closed process expression E′ such that E ⟶^{α} E′ and P′ = E′[P/X], or X is exposed in E and P ⟶^{α} P′. In the first case, since E \underline{↔}_{rbX}^{Δ} F, there exist a process expression F′ such that F ⟶^{α} F′ and E′ \underline{↔}_{bX}^{Δ} F′. By Lemma 9.1 F[P/X] ⟶^{α} F′[P/X]. Furthermore, by Lemma 13 P′ = E′[P/X] \underline{↔}_{b}^{Δ} F′[P/X]. In the second case, since X is exposed in E we have that E ⟶^{X} 0, and hence, since E \underline{↔}_{rbX}^{Δ} F, there exists a process expression F′ such that F ⟶^{X} F′. By Lemma 9.1 F[P/X] ⟶^{α} P′. Furthermore, P′ \underline{↔}_{b}^{Δ} P′. The other clause follows by symmetry, thus yielding E[P/X] \underline{↔}_{rb}^{Δ} F[P/X].

“If”: Let E and F be X-closed process expressions. Since by Proposition 12 the set of all process expressions reachable from E and F is finite, there exists a natural number n ∈ ω such that for all G reachable from E or F it holds that G \underline{↮}_{b}^{Δ} a^{n}, and thus G[a^{n+1}/X] \underline{↮}_{b}^{Δ} a^{n}. Let

R = \{(E′, F′) | E ⟶^{∗} E′, F ⟶^{∗} F′, E′[a^{n+1}/X] \underline{↔}_{b}^{Δ} F′[a^{n+1}/X]\}.

Claim: The symmetric closure of R is a branching bisimulation satisfying (D′′) w.r.t. the V ⊎ A_{τ} - labelled transition relation.

Proof of the claim: To prove that R satisfies condition (T) of Definition 1, let E′ and F′ be such that E′ R F′, and suppose that E′ ⟶^{α} E′′. Then E′[a^{n+1}/X] \underline{↔}_{b}^{Δ} F′[a^{n+1}/X] and, using Lemma 9.1, E′[a^{n+1}/X] ⟶^{α} E′′[a^{n+1}/X]. Since E′[a^{n+1}/X] \underline{↔}_{b}^{Δ} F′[a^{n+1}/X] there exist closed

process expressions Q′′′ and Q′′ such that F′[a^{n+1}/X] −↠ Q′′ ⟶^{(α)} Q′′′, E′[a^{n+1}/X] \underline{↔}_{b}^{Δ} Q′′

and E′′[a^{n+1}/X] \underline{↔}_{b}^{Δ} Q′′′. By Lemma 9.2, using that a ≠ τ, there exists a X-closed process expression F′′ such that F′ −↠ F′′ and Q′′ = F′′[a^{n+1}/X]; moreover, either there exists an Xclosed process expression F′′′ such that F′′ ⟶^{(α)} F′′′ and Q′′′ = F′′′[a^{n+1}/X], or X is exposed in F′′ and a^{n+1} ⟶^{α} Q′′′. In the latter case we would have E′′[a^{n+1}/X] \underline{↔}_{b}^{Δ} Q′′′ = a^{n}, which is impossible by the choice of n. So the former case applies: we have F′ −↠ F′′ ⟶^{(α)} F′′′, E′ R F′′ and E′′ R F′′′. The case that F′ ⟶^{α} F′′ proceeds by symmetry, so the symmetric closure of R satisfies condition (T).

To show that R (and its symmetric closure) satisfies (D′′), let (E_{k})_{k∈ω} be an infinite sequence of X-closed process expressions such that E_{k} ⟶^{τ} E_{k+1} for all k ∈ ω, and let F_{0} be such that E_{0} R F_{0}.

Then E_{0}[a^{n+1}/X] \underline{↔}_{b}^{Δ} F_{0}[a^{n+1}/X] and by Lemma 9.1 E_{k}[a^{n+1}/X] ⟶^{τ} E_{k+1}[a^{n+1}/X] for all k∈ω.

Using (D′′), there exist a process expression Q′ such that F_{0} ⟶^{τ} Q′ and E_{k}[a^{n+1}/X] \underline{↔}_{b}^{Δ} Q′ for some k ∈ N. By Lemma 9.2, using that a ≠ τ, there exists a X-closed process expression F′ such that F_{0} ⟶^{τ} F′ and Q′ = F′[a^{n+1}/X]. Furthermore, E_{k} R F′.

Application of the claim: Let E[P/X] \underline{↔}_{b}^{Δ} F[P/X] for each closed process expression P. Then E[a^{n+1}/X] \underline{↔}_{b}^{Δ} F[a^{n+1}/X]. The claim yields E \underline{↔}_{bX}^{Δ} F.

Now let E[P/X] \underline{↔}_{rb}^{Δ} F[P/X] for each closed P. Then E[a^{n+1}/X] \underline{↔}_{rb}^{Δ} F[a^{n+1}/X]. Suppose that E ⟶^{α} E′ with α ∈ A_{τ}. Then E[a^{n+1}/X] ⟶^{α} E′[a^{n+1}/X] by Lemma 9.1. So there exists a Q′ with F[a^{n+1}/X] ⟶^{α} Q′ and E′[a^{n+1}/X] \underline{↔}_{b}^{Δ} Q′. By Lemma 9.2 either there exists an X-closed process expression F′ such that F ⟶^{α} F′ and Q′ = F′[a^{n+1}/X], or X is exposed in F and a^{n+1} ⟶^{α} Q′. In the latter case we would have E′[a^{n+1}/X] \underline{↔}_{b}^{Δ} Q′ = a^{n}, which is impossible by the choice of n. So the former case applies, and E′ R F′. The claim yields E′ \underline{↔}_{bX}^{Δ} F′. The other clause follows by symmetry, so E \underline{↔}_{rbX}^{Δ} F.

The following is an immediate corollary of Propositions 14, 3 and 4.

Corollary 15. Let E and F be X-closed process expressions such that E \underline{↔}_{b}^{Δ} F.

1. If E ⟶^{α} E′, then there exist X-closed process expressions F_{0}, …, F_{n} and F′ such that

F = F_{0} ⟶^{τ} ⋯ ⟶^{τ} F_{n} ⟶^{(α)} F′ such that E \underline{↔}_{b}^{Δ} F_{i} (0 ≤ i ≤ n) and E′ \underline{↔}_{b}^{Δ} F′.

2. If X is exposed in E, then there exist k ≥ 0 and X-closed process expressions F_{0}, …, F_{k} such that F = F_{0} ⟶^{τ} ⋯ ⟶^{τ} F_{k}, E \underline{↔}_{b}^{Δ} F_{i} (0 ≤ i ≤ k), and X is exposed in F_{k}.

3. If there is an infinite sequence of X-closed process expressions (E_{k})_{k∈ω} such that E = E_{0} and E_{k} ⟶^{τ} E_{k+1}, then there exists an X-closed process expression F′ such that F ⟶^{τ} F′ and E_{k} \underline{↔}_{b}^{Δ} F′ for some k ∈ ω.

Similarly, by combining Propositions 14 and Definition 5 we get the following corollary.

Corollary 16. Let E and F be X-closed process expressions such that E \underline{↔}_{rb}^{Δ} F. If E ⟶^{α} E′, then there exists an X-closed process expression F′ such that F ⟶^{α} F′ and E′ \underline{↔}_{b}^{Δ} F′.

3.2 Rooted divergence-preserving branching bisimulation up to \underline{↔}_{b}^{Δ}

As was already illustrated by Milner [20], a suitable up-to relation is a crucial tool in the proof that a behavioural equivalence is compatible with the recursion construct. In [7], Milner’s notion of weak bisimulation up to weak bisimilarity is adapted to branching bisimulation up to branching bisimilarity. Here we make two further modifications. Not only do we add a divergence condition; we also incorporate rootedness into the relation.

Definition 17. Let R be a symmetric binary relation on P, and denote by R^{u} the relation \underline{↔}_{b}^{Δ} ; R; \underline{↔}_{b}^{Δ}. We say that R is a rooted divergence-preserving branching bisimulation up to \underline{↔}_{b}^{Δ} if for all P, Q ∈ P such that P R Q the following three conditions are satisfied:

(U1) if P ⟶^{α} P′, then there exist Q′ such that Q ⟶^{α} Q′, and P′ R^{u} Q′.

(U2) if P −↠ P′′ ⟶^{(α)} P′, then there exist Q′ and Q′′ such that Q −↠ Q′′ ⟶^{(α)} Q′, P′′ R^{u} Q′′ and

P′ R^{u} Q′.

(U3) if there exists an infinite sequence of closed process expressions (P_{k})_{k∈ω} such that P = P_{0}, and P_{k} ⟶^{τ} P_{k+1} for all k ∈ ω, then there also exists an infinite sequence of closed process expressions (Q_{ℓ})_{ℓ∈ω} and a mapping σ : ω → ω such that Q = Q_{0}, and Q_{ℓ} ⟶^{τ} Q_{ℓ+1} and P_{σ(ℓ)} R^{u} Q_{ℓ} for all ℓ ∈ ω.

Proposition 18. Let P and Q be closed process expressions and let R be a rooted divergencepreserving branching bisimulation up to \underline{↔}_{b}^{Δ}. If P R Q, then P \underline{↔}_{rb}^{Δ} Q.

Proof. If P R Q and P ⟶^{α} P′, then since R satisfies condition (U1) of Definition 17, there exists a Q′ such that Q ⟶^{α} Q′ and P′ R^{u} Q′. Furthermore, since R is symmetric, whenever P R Q also Q R P, so if Q ⟶^{α} Q′, then by condition (U1) of Definition 17 there exists a P′ such that P ⟶^{α} P′ and Q′ R^{u} P′. It remains to establish that P′ \underline{↔}_{b}^{Δ} Q′, and for this, it suffices by Proposition 3 to prove that R^{u} is a branching bisimulation satisfying (D′).

Note that, since \underline{↔}_{b}^{Δ} and R are both symmetric, also R^{u} is symmetric.

To prove that R^{u} satisfies (T), let P_{0}, P_{1}, Q_{0} and Q_{1} be closed process expressions such that P_{1} \underline{↔}_{b}^{Δ} P_{0} R Q_{0} \underline{↔}_{b}^{Δ} Q_{1}, and suppose that P_{1} ⟶^{α} P′_{1}. Since P_{1} \underline{↔}_{b}^{Δ} P_{0} and \underline{↔}_{b}^{Δ} satisfies (T), there exist P′_{0} and P′′_{0} such that P_{0} −↠ P′′_{0} ⟶^{(α)} P′_{0}, P_{1} \underline{↔}_{b}^{Δ} P′′_{0} and P′_{1} \underline{↔}_{b}^{Δ} P′_{0}. So it follows by condition (U2) of Definition 17 that there exist Q′_{0} and Q′′_{0} such that Q_{0} −↠ Q′′_{0} ⟶^{(α)} Q′_{0}, P′′_{0} R^{u} Q′′_{0} and P′_{0} R^{u} Q′_{0}. Hence, since Q_{0} \underline{↔}_{b}^{Δ} Q_{1}, by Lemma 2 there exist closed process expressions Q′_{1} and Q′′_{1} such that Q_{1} −↠ Q′′_{1} ⟶^{(α)} Q′_{1}, Q′′_{0} \underline{↔}_{b}^{Δ} Q′′_{1} and Q′_{0} \underline{↔}_{b}^{Δ} Q′_{1}. Note, moreover, that P_{1} \underline{↔}_{b}^{Δ} P′′_{0} R^{u} Q′′_{0} \underline{↔}_{b}^{Δ} Q′′_{1} whence P_{1} R^{u} Q′′_{1}, and P′_{1} \underline{↔}_{b}^{Δ} P′_{0} R^{u} Q′_{0} \underline{↔}_{b}^{Δ} Q′_{1} whence P′_{1} R^{u} Q′_{1}.

It remains to prove that R^{u} satisfies (D′) of Proposition 3. To this end, let P_{0}, P_{1}, Q_{0} and Q_{1} be closed process expressions such that P_{1} \underline{↔}_{b}^{Δ} P_{0} R Q_{0} \underline{↔}_{b}^{Δ} Q_{1}, and suppose that there exists an infinite sequence of closed process expressions (P_{1,k})_{k∈ω} such that P_{1} = P_{1,0} and P_{1,k} ⟶^{τ} P_{1,k+1}. Then, since P_{1} \underline{↔}_{b}^{Δ} P_{0}, by Proposition 3, there exists an infinite sequence of closed process expressions (P_{0,k})_{ℓ∈ω} and a mapping σ_{P} : ω → ω such that P_{0} = P_{0,0}, P_{0,ℓ} ⟶^{τ} P_{0,ℓ+1} and P_{1,σ_{P} (ℓ)} \underline{↔}_{b}^{Δ} P_{0,ℓ} for all ℓ ∈ ω. Hence, since P_{0} R Q_{0} and R is a divergence-preserving branching bisimulation up to \underline{↔}_{b}^{Δ}, there exists an infinite sequence of closed process expressions (Q_{0,m})_{m∈ω}

and a mapping σ_{P,Q} : ω → ω such that Q_{0} = Q_{0,0}, Q_{0,m} ⟶^{τ} Q_{0,m+1} and P_{0,σ_{P,Q} (m)} R^{u} Q_{0,m} for

all m ∈ ω. Hence, since Q_{0} \underline{↔}_{b}^{Δ} Q_{1}, by Proposition 3, there exists an infinite sequence of closed process expressions (Q_{1,n})_{n∈ω} and a mapping σ_{Q} : ω → ω such that Q_{1} = Q_{1,0}, Q_{1,n} ⟶^{τ} Q_{0,n+1} and Q_{0,σ_{Q} (n)} \underline{↔}_{b}^{Δ} Q_{1,n} for all n ∈ ω. We define

σ = σ_{P} ∘ σ_{P,Q} ∘ σ_{Q} ,

and then we have that P_{1,σ(n)} \underline{↔}_{b}^{Δ} ; R^{u} ; \underline{↔}_{b}^{Δ} Q_{1,n}, and hence P_{1,σ(n)} R^{u} Q_{1,n} for all n ∈ ω.

To prove that \underline{↔}_{rb}^{Δ} is compatible with μX. means to prove that if E \underline{↔}_{rb}^{Δ} F, then μX.E \underline{↔}_{rb}^{Δ} μX.F. We first do this in the special case that E and F are X-closed. A crucial step in this proof will be to show that if E \underline{↔}_{rb}^{Δ} F for X-closed process expressions E and F, then the symmetric closure R_{E,F} of the relation

{(G[μX.E/X], G[μX.F/X]) | G ∈ E, FV (G) ⊆ {X}} (1)

is a rooted branching bisimulation up to \underline{↔}_{b}^{Δ}. The result then follows by taking G := X. Until Corollary 25 we fix X-closed process expressions E and F such that E \underline{↔}_{rb}^{Δ} F.

Lemma 19. For all X-closed process expressions G, if G[μX.E/X] ⟶^{α} P, then there exists a Q

such that G[μX.F/X] ⟶^{α} Q and P R_{E,F} ; \underline{↔}_{b}^{Δ} Q.

Proof. Let G be an X-closed process expression, and suppose that G[μX.E/X] ⟶^{α} P; we proceed with induction on a derivation of this transition. By Lemma 9.2 there are two cases: either the transition under consideration stems directly from G, i.e., there exists a G′ such that G ⟶^{α} G′ and P = G′[μX.E/X], or X is exposed in G, μX.E ⟶^{α} P and every derivation of G[μX.E/X] ⟶^{α} P has a derivation of μX.E ⟶^{α} P as a subderivation.

In the first case, Lemma 9.1 implies G[μX.F/X] ⟶^{α} G′[μX.F/X] and P = G′[μX.E/X] R_{E,F} G′[μX.F/X], so, since \underline{↔}_{b}^{Δ} is reflexive, also P R_{E,F} ; \underline{↔}_{b}^{Δ} G′[μX.F/X].

In the second case, since the considered derivation of the transition G[μX.E/X] ⟶^{α} P has a derivation of μX.E ⟶^{α} P as a subderivation, and the last rule applied in this subderivation must be rule 2, it follows that the considered derivation of G[μX.E/X] ⟶^{α} P has a derivation of E[μX.E/X] ⟶^{α} P as a proper subderivation. So by the induction hypothesis there exists a Q such that E[μX.F/X] ⟶^{α} Q and P R_{E,F} ; \underline{↔}_{b}^{Δ} Q. Furthermore, since E \underline{↔}_{rb}^{Δ} F, whence E[μX.F/X] \underline{↔}_{rb}^{Δ} F[μX.F/X], it follows that there exists an R such that F[μX.F/X] ⟶^{α} R and Q \underline{↔}_{b}^{Δ} R. It follows from F[μX.F/X] ⟶^{α} R that μX.F ⟶^{α} R. Since X is exposed in G, Lemma 9.1 yields G[μX.F/X] ⟶^{α} R. From P R_{E,F} ; \underline{↔}_{b}^{Δ} Q and Q \underline{↔}_{b}^{Δ} R it follows that P R_{E,F} ; \underline{↔}_{b}^{Δ} R.

As an immediate corollary to Lemma 19 we get that if E \underline{↔}_{rb}^{Δ} F, then R_{E,F} satisfies the first condition of rooted divergence-preserving branching bisimulations up to \underline{↔}_{b}^{Δ}.

Corollary 20. R_{E,F} satisfies condition (U1) of Definition 17.

With a little more work, Lemma 19 can also be used to derive that R_{E,F} satisfies the second condition of rooted divergence-preserving branching bisimulations up to \underline{↔}_{b}^{Δ}. To this end, we first prove the following lemma.

Lemma 21. Let P and Q be closed process expressions. If P R_{E,F} ; \underline{↔}_{b}^{Δ} Q and P ⟶^{α} P′, then

there exist Q′ and Q′′ such that Q −↠ Q′′ ⟶^{(α)} Q′, P R_{E,F} ; \underline{↔}_{b}^{Δ} Q′′ and P′ R_{E,F} ; \underline{↔}_{b}^{Δ} Q′.

Proof. Suppose that P R_{E,F} ; \underline{↔}_{b}^{Δ} Q and P ⟶^{α} P′. Then there exists an R such that P R_{E,F} R \underline{↔}_{b}^{Δ} Q, and according to the definition of R_{E,F} there exists an X-closed process expression G such that either P = G[μX.E/X] and R = G[μX.F/X] or P = G[μX.F/X] and R = G[μX.E/X]. There is clearly no loss of generality in assuming that P = G[μX.E/X] and R = G[μX.F/X]. By Lemma 19, there exists an R′ such that R ⟶^{α} R′ and P′ R_{E,F} ; \underline{↔}_{b}^{Δ} R′. Hence, since R \underline{↔}_{b}^{Δ} Q, there exist Q′ and Q′′ such that Q −↠ Q′′ ⟶^{(α)} Q′, R \underline{↔}_{b}^{Δ} Q′′ and R′ \underline{↔}_{b}^{Δ} Q′. It follows that P R_{E,F} ; \underline{↔}_{b}^{Δ} Q′′ and P′ R_{E,F} ; \underline{↔}_{b}^{Δ} Q′, so the proof of the lemma is complete.

Applying Lemma 21 with induction on the length of a transition sequence that gives rise to P −↠ P′′ ⟶^{α} P′, it is straightforward to establish the following corollary.

Corollary 22. R_{E,F} satisfies condition (U2) of Definition 17.

Proof. Let P_{n}, …, P_{0}, P′, Q ∈ P, such that P_{n} R_{E,F} ; \underline{↔}_{b}^{Δ} Q, P_{i+1} ⟶^{τ} P_{i} for all 0 ≤ i < n, and

P_{0} ⟶^{(α)} P′; we prove with induction on n that there exists Q′ and Q′′ such that Q −↠ Q′′ ⟶^{(α)} Q′ P_{0} R_{E,F} ; \underline{↔}_{b}^{Δ} Q′′, and P′ R_{E,F} ; \underline{↔}_{b}^{Δ} Q′. Note that, since \underline{↔}_{b}^{Δ} is reflexive, it then follows that R_{E,F} satisfies (U2) of Definition 17.

If n = 0, then we distinguish two cases: If α = τ and P_{0} = P′, then we can take Q′′ = Q′ = Q. If α ≠ τ or P_{0} ≠ P′, then P_{0} ⟶^{α} P′, and the result follows from Lemma 21.

Suppose that n > 0. Then P_{n} ⟶^{τ} P_{n−1}, so by Lemma 21 there exist Q_{n} and Q_{n−1} such

that Q −↠ Q_{n} ⟶^{(τ)} Q_{n−1}, P_{n} R_{E,F} ; \underline{↔}_{b}^{Δ} Q_{n}, and P_{n−1} R_{E,F} ; \underline{↔}_{b}^{Δ} Q_{n−1}. Furthermore, by the

induction hypothesis, there exist Q′ and Q′′ such that Q_{n−1} −↠ Q′′ ⟶^{(α)} Q′, P_{0} R_{E,F} ; \underline{↔}_{b}^{Δ} Q′′, and P′ R_{E,F} ; \underline{↔}_{b}^{Δ} Q′. Clearly, we then also have that Q −↠ Q′′ ⟶^{(α)} Q′.

It remains to establish that R_{E,F} satisfies the third condition of rooted divergence-preserving branching bisimulations up to \underline{↔}_{b}^{Δ}.

Lemma 23. Let G and H be X-closed process expressions such that G \underline{↔}_{b}^{Δ} H. If there exists an infinite sequence of closed process expressions (P_{k})_{k∈ω} such that G[μX.E/X]=P_{0} and P_{k} ⟶^{τ} P_{k+1} for all k ∈ ω, then there also exists an infinite sequence of closed process expressions (Q_{ℓ})_{ℓ∈ω} and

a mapping σ : ω → ω such that H[μX.F/X] = Q_{0}, Q_{ℓ} ⟶^{τ} Q_{ℓ+1}, and P_{σ(ℓ)} R_{E,F} ; \underline{↔}_{b}^{Δ} Q_{ℓ} for all

ℓ ∈ ω.

Proof. Suppose that there exists an infinite sequence of closed process expressions (P_{k})_{k∈ω} such that G[μX.E/X] = P_{0} and P_{k} ⟶^{τ} P_{k+1} for all k ∈ ω. By Corollary 11 there is an infinite sequence of X-closed process expressions (G_{k})_{k∈ω} such that P_{k} = G_{k}[μX.E/X] and either G_{k} ⟶^{τ} G_{k+1} or E ⟶^{τ} G_{k+1} for all k ∈ ω. We shall define simultaneously, with induction on ℓ, an infinite sequence of X-closed process expressions (H_{ℓ})_{ℓ∈ω} with H_{0} = H and H_{ℓ}[μX.F/X] ⟶^{τ} H_{ℓ+1}[μX.F/X], and a mapping σ : ω → ω, such that G_{σ(ℓ)} \underline{↔}_{b}^{Δ} H_{ℓ}. This will suffice, because, for all ℓ ∈ ω, defining Q_{ℓ}

as H_{ℓ}[μX.F/X] we obtain Q_{ℓ} ⟶^{τ} Q_{ℓ+1} and P_{σ(ℓ)} = G_{σ(ℓ)}[μX.E/X] R_{E,F} G_{σ(ℓ)}[μX.F/X] \underline{↔}_{b}^{Δ}

H_{ℓ}[μX.F/X] = Q_{ℓ}.

Suppose, by way of induction hypothesis, that H_{ℓ} and σ(ℓ) have been defined already, such that G_{σ(ℓ)} \underline{↔}_{b}^{Δ} H_{ℓ}. By Corollary 11 there are two cases:

1. G_{σ(ℓ)+k} ⟶^{τ} G_{σ(ℓ)+k+1} for all k ∈ ω. Then, since G_{σ(ℓ)} \underline{↔}_{b}^{Δ} H_{ℓ}, by Corollary 15.3 there exists an X-closed process expression H′ such that H_{ℓ} ⟶^{τ} H′ and G_{σ(ℓ)+k} \underline{↔}_{b}^{Δ} H′ for some

k ∈ ω. We define H_{ℓ+1} = H′ and σ(ℓ + 1) = σ(ℓ) + k. Now H_{ℓ}[μX.F/X] ⟶^{τ} H_{ℓ+1}[μX.F/X]

by Lemma 9.1 and G_{σ(ℓ+1)} \underline{↔}_{b}^{Δ} H_{ℓ+1}.

2. There is a k ∈ ω such that G_{σ(ℓ)+i} ⟶^{τ} G_{σ(ℓ)+i+1} for all i < k, X is exposed in G_{σ(ℓ)+k} and E ⟶^{τ} G_{σ(ℓ)+k+1}. Then, since G_{σ(ℓ)} \underline{↔}_{b}^{Δ} H_{ℓ}, by Corollary 15.1 and with induction on i there exists a sequence H′_{0}, …, H′_{m} and a mapping ρ : {0, …, m} → {0, …, k} with ρ(m)=k such that H_{ℓ} = H′_{0} ⟶^{τ} ⋯ ⟶^{τ} H′_{m} and G_{σ(ℓ)+ρ(j)} \underline{↔}_{b}^{Δ} H′_{j}. Using Corollary 15.2, we may furthermore assume that X is exposed in H′_{m}.

If m > 0, then we define H_{ℓ+1} = H′_{1} and σ(ℓ + 1) = σ(ℓ) + ρ(1). Now H_{ℓ}[μX.F/X] ⟶^{τ} H_{ℓ+1}[μX.F/X] by Lemma 9.1 and G_{σ(ℓ+1)} \underline{↔}_{b}^{Δ} H_{ℓ+1}.

So it remains to consider the case that m = 0. Since E \underline{↔}_{rb}^{Δ} F, there exists, by Corollary 16, an X-closed process expression F′ such that F ⟶^{τ} F′ and G_{σ(ℓ)+k+1} \underline{↔}_{b}^{Δ} F′. We now define H_{ℓ+1} = F′ and σ(ℓ + 1) = σ(ℓ) + k + 1. We then have that G_{σ(ℓ+1)} = G_{σ(ℓ)+k+1} \underline{↔}_{b}^{Δ} H_{ℓ+1},

and F[μX.F/X] ⟶^{τ} H_{j+1}[μX.F/X] by Lemma 9.1. So μX.F ⟶^{τ} H_{j+1}[μX.F/X] by rule 2,

and Lemma 9.1 yields H_{ℓ}[μX.F/X] ⟶^{τ} H_{ℓ+1}[μX.F/X], using that X is exposed in H_{ℓ}.

From Lemma 23 with G = H we immediately get the following corollary.

Corollary 24. R_{E,F} satisfies condition (U3) of Definition 17.

The relation R_{E,F} is symmetric by definition and we have now also proved that it satisfies conditions (U1), (U2) and (U3), so we have established the following result.

Corollary 25. R_{E,F} is a rooted divergence-preserving branching bisimulation up to \underline{↔}_{b}^{Δ}.

3.3 The main results

We can now establish that \underline{↔}_{rb}^{Δ} is compatible with α., μX. and +.

Proposition 26. If E \underline{↔}_{rb}^{Δ} F, then α.E \underline{↔}_{rb}^{Δ} α.F for all α ∈ A_{τ}, E + H \underline{↔}_{rb}^{Δ} F + H and H + E \underline{↔}_{rb}^{Δ} H + F for all process expressions H, and μX.E \underline{↔}_{rb}^{Δ} μX.F.

Proof. To prove that \underline{↔}_{rb}^{Δ} is compatible with α. and + is straightforward. (First, establish the property for closed terms, and then use that substitution distributes over α. and +.)

It remains to prove that \underline{↔}_{rb}^{Δ} is compatible with μX. , i.e., that E \underline{↔}_{rb}^{Δ} F implies μX.E \underline{↔}_{rb}^{Δ} μX.F. Note that in the special case that E and F are X-closed this immediately follows from Corollary 25 and Proposition 18. Now, for the general case, let E and F be process expressions and suppose that E \underline{↔}_{rb}^{Δ} F. Let X, Y⃗ be a sequence of variables that at least includes the variables with a free occurrence in E or F, and such that X does not occur in Y⃗. Then, according to the definition of \underline{↔}_{rb}^{Δ} on process expressions with free variables (Definition 7), we have that, for every closed process expression P and for every sequence of closed process expressions P⃗ of the same length as Y⃗, E[P, P⃗/X, Y⃗] \underline{↔}_{rb}^{Δ} F[P, P⃗/X, Y⃗]. So, clearly, also E[P⃗/Y⃗] \underline{↔}_{rb}^{Δ} F[P⃗/Y⃗], and since E[P⃗/Y⃗] and F[P⃗/Y⃗] are X-closed, it follows that μX.E[P⃗/Y⃗] \underline{↔}_{rb}^{Δ} μX.F[P⃗/Y⃗]. Since X is not among the Y⃗, we may conclude that (μX.E)[P⃗/Y⃗] \underline{↔}_{rb}^{Δ} (μX.F)[P⃗/Y⃗] for every sequence of closed process expressions P⃗ of the same length as Y⃗, and hence μX.E \underline{↔}_{rb}^{Δ} μX.F.

We have now obtained our main result that \underline{↔}_{rb}^{Δ} is a congruence. In fact, it is the coarsest contained in \underline{↔}_{b}^{Δ}.

Theorem 27. The relation \underline{↔}_{rb}^{Δ} is the coarsest congruence contained in \underline{↔}_{b}^{Δ}.

Proof. By Propositions 6 and 26, the relation \underline{↔}_{rb}^{Δ} is a congruence. To prove that it is coarsest, it suffices to prove that for every relation R ⊆ \underline{↔}_{b}^{Δ} that is compatible with + we have that R ⊆ \underline{↔}_{rb}^{Δ}. Let P and Q be closed process expressions, and suppose that P R Q.

Since by Proposition 12 the set of closed process expressions reachable from P and Q is finite and A is non-empty, there exists a natural number n ∈ ω such that for all R reachable from P or Q it holds that R \underline{↮}_{b}^{Δ} a^{n}. This implies that for all R reachable from P or Q it holds that R \underline{↮}_{b}^{Δ} P + a^{n+1} and R \underline{↮}_{b}^{Δ} Q + a^{n+1}.

Since R is compatible with +, we have that P + a^{n+1} R Q + a^{n+1}, and hence P + a^{n+1} \underline{↔}_{b}^{Δ} Q + a^{n+1}. To prove (R1), suppose that P ⟶^{α} P′. Then P + a^{n+1} ⟶^{α} P′, so by Lemma 2 there exist closed process expressions Q′ and Q′′ such that Q + a^{n+1} −↠ Q′′ ⟶^{(α)} Q′, P + a^{n+1} \underline{↔}_{b}^{Δ} Q′′ and P′ \underline{↔}_{b}^{Δ} Q′. Since a ≠ τ, we have that Q′′ = Q + a^{n+1}, for otherwise Q′′ is reachable from Q and Q′′ \underline{↔}_{b}^{Δ} P + a^{n+1}. Moreover, Q′′ ⟶^{α} Q′, for otherwise P′ \underline{↔}_{b}^{Δ} Q′ = Q′′ = Q + a^{n+1}. Condition (R2) follows by symmetry.

References

[1] Jos C. M. Baeten, Bas Luttik & Paul van Tilburg (2012): Turing Meets Milner. In Maciej Koutny & Irek Ulidowski, editors: Proceedings 23rd International Conference on Concurrency Theory, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012, LNCS 7454, Springer, pp. 1–20, doi:10.1007/978-3-642-32940-1 1.

[2] Jos C. M. Baeten, Bas Luttik & Paul van Tilburg (2013): Reactive Turing machines. Inf. Comput. 231, pp. 143–166, doi:10.1016/j.ic.2013.08.010.

[3] Jos C. M. Baeten, Bas Luttik & Fei Yang (2017): Sequential Composition in the Presence of Intermediate Termination (Extended Abstract). In Kirstin Peters & Simone Tini, editors: Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics, EXPRESS/SOS 2017, Berlin, Germany, 4th September 2017, EPTCS 255, pp. 1–17, doi:10.4204/EPTCS.255.1.

[4] Wan Fokkink, Rob van Glabbeek & Bas Luttik (2017): Divide and Congruence III: Stability & Divergence. In: Proceedings 28th International Conference on Concurrency Theory, CONCUR 2017, Leibniz International Proceedings in Informatics (LIPIcs) 85, pp. 15:1–15:16, doi:10.4230/LIPIcs.CONCUR.2017.15.

[5] David de Frutos Escrig, Jeroen J. A. Keiren & Tim A. C. Willemse (2016): Branching Bisimulation Games. In Elvira Albert & Ivan Lanese, editors: Proceedings 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2016, held as part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, LNCS 9688, Springer, pp. 142–157, doi:10.1007/978-3-319-39570-8 10.

[6] Yuxi Fu (2016): Theory of interaction. Theoretical Computer Science 611, pp. 1–49, doi:10.1016/j.tcs.2015.07.043.

[7] Rob J. van Glabbeek (1993): A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In A.M. Borzyszkowski & S. Sokołowski, editors: Proceedings 18^{th} International Symposium on Mathematical Foundations of Computer Science, MFCS ’93, Gdansk, Poland, August/September 1993, LNCS 711, Springer, pp. 473–484, doi:10.1007/3-540-57182-5 39.

[8] Rob J. van Glabbeek (1993): The Linear Time – Branching Time Spectrum II; The semantics of sequential systems with silent moves (extended abstract). In E. Best, editor: Proceedings 4^{th} International Conference on Concurrency Theory, CONCUR’93, Hildesheim, Germany, August 1993, LNCS 715, Springer, pp. 66–81, doi:10.1007/3-540-57208-2 6.

[9] Rob J. van Glabbeek (2001): What is branching time semantics and why to use it? In G. Paun, G. Rozenberg & A. Salomaa, editors: Current Trends in Theoretical Computer Science; Entering the 21st Century, World Scientific, pp. 469–479.

Available at http://Theory.stanford.edu/~rvg/branching. Also in M. Nielsen, editor:

The Concurrency Column, Bulletin of the EATCS 53, 1994, pp. 190–198.

[10] Rob J. van Glabbeek (2017): Lean and Full Congruence Formats for Recursion. In: Proceedings 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, IEEE Computer Society Press, pp. 1–11, doi:10.1109/LICS.2017.8005142.

[11] Rob J. van Glabbeek, Bas Luttik & Nikola Trčka (2009): Branching Bisimilarity with Explicit Divergence. Fundamenta Informaticae 93(4), pp. 371–392, doi:10.3233/FI-2009-109.

[12] Rob J. van Glabbeek, Bas Luttik & Nikola Trčka (2009): Computation Tree Logic with Deadlock Detection. Logical Methods in Computer Science 5(4), doi:10.2168/LMCS-5(4:5)2009.

[13] Rob J. van Glabbeek & W. Peter Weijland (1996): Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), pp. 555–600, doi:10.1145/233551.233556.

[14] Daniele Gorla (2010): Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9), pp. 1031–1053, doi:10.1016/j.ic.2010.05.002.

[15] Markus Lohrey, Pedro R. D’Argenio & Holger Hermanns (2005): Axiomatising divergence. Inf. Comput. 203(2), pp. 115–144, doi:10.1016/j.ic.2005.05.007.

[16] Bas Luttik & Fei Yang (2015): Executable Behaviour and the π-Calculus (extended abstract). In Sophia Knight, Ivan Lanese, Alberto Lluch-Lafuente & Hugo Torres Vieira, editors: Proceedings 8th Interaction and Concurrency Experience, ICE 2015, Grenoble, France, 4-5th June 2015, EPTCS 189, pp. 37–52, doi:10.4204/EPTCS.189.5.

[17] Bas Luttik & Fei Yang (2016): On the Executability of Interactive Computation. In Arnold Beckmann, Laurent Bienvenu & Natasa Jonoska, editors: Proceedings Pursuit of the Universal - 12th Conference on Computability in Europe, CiE 2016, Paris, France, June 27 - July 1, 2016, LNCS 9709, Springer, pp. 312–322, doi:10.1007/978-3-319-40189-8 32.

[18] Radu Mateescu &Anton Wijs (2014): Property-dependent reductions adequate with divergencesensitive branching bisimilarity. Science of Computer Programming 96, pp. 354–376, doi:10.1016/j.scico.2014.04.004.

[19] Robin Milner (1989): A Complete Axiomatisation for Observational Congruence of Finite-State Behaviors. Inf. Comput. 81(2), pp. 227–247, doi:10.1016/0890-5401(89)90070-9.

[20] Robin Milner (1990): Operational and Algebraic Semantics of Concurrent Processes. In Jan van Leeuwen, editor: Handbook of Theoretical Computer Science (Vol. B), MIT Press, Cambridge, MA, USA, pp. 1201–1242.

Available at http://dl.acm.org/citation.cfm?id=114891.114910.

[21] Iain Phillips (1993): A Note on Expressiveness of Process Algebra. In Geoffrey L. Burn, Simon J. Gay & Mark Ryan, editors: Proceedings of the First Imperial College Department of Computing Workshop on Theory and Formal Methods, Isle of Thorns Conference Centre, Chelwood Gate, Sussex, UK, 29-31 March 1993, Workshops in Computing, Springer, pp. 260–264.

[22] Sander de Putter & Anton Wijs (2017): Compositional Model Checking Is Lively. In José Proença & Markus Lumpe, editors: Proceedings 14th International Conference on Formal Aspects of Component Software, FACS 2017, Braga, Portugal, October 10-13, 2017, LNCS 10487, Springer, pp. 117–136, doi:10.1007/978-3-319-68034-7 7.

[23] F.W. Vaandrager (1990): Algebraic Techniques for Concurrency and their Application. Ph.D. thesis, University of Amsterdam.

[24] Anton Wijs & Luc Engelen (2013): Efficient Property Preservation Checking of Model Refinements. In Nir Piterman & Scott A. Smolka, editors: Proceedings 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, LNCS 7795, Springer, pp. 565–579, doi:10.1007/978-3-642-36742-7 41.

[25] Xian Xu (2012): Distinguishing and relating higher-order and first-order processes by expressiveness. Acta Informatica 49(7-8), pp. 445–484, doi:10.1007/s00236-012-0168-9.

[26] Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng & Chris J. Myers (2016): An improved fault-tolerant routing algorithm for a Network-on-Chip derived with formal analysis. Sci. of Computer Programming 118, pp. 24–39, doi:10.1016/j.scico.2016.01.002.