A Characterisation of Weak Bisimulation Congruence

Rob van Glabbeek

National ICT Australia and School of Computer Science and Engineering The University of New South Wales

                           rvg@cs.stanford.edu

Abstract. This paper shows that weak bisimulation congruence can be characterised as rooted weak bisimulation equivalence, even without making assumptions on the cardinality of the sets of states or actions of the processes under consideration.

Introduction

Weak bisimulation equivalence, also known as observation equivalence [Mil90], is a fundamental semantic equivalence used in system verification, and one of the first proposed in the literature. It upgrades strong bisimulation equivalence by featuring abstraction from internal actions.

In order to allow compositional system verification, semantic equivalence relations need to be congruences for the operators under consideration, meaning that the equivalence class of an n-ary operator f applied to arguments p_{1}, …, p_{n} is completely determined by the equivalence classes of these arguments. Although strong bisimulation equivalence is a congruence for the operators of CCS, ACP_{τ} and many other languages found in the literature, weak bisimulation equivalence fails to be a congruence for the choice or alternative composition operator + of CCS, as well as for the left-merge ∥− of ACP_{τ}. To bypass this problem, one uses the coarsest congruence relation for + that is finer than weak bisimulation equivalence, called weak bisimulation congruence, and characterised as rooted weak bisimulation equivalence in [BK85]. This equivalence turns out to be a minor variant of weak bisimulation equivalence, and a congruence for all of CCS, ACP_{τ} and many other languages.

Classical proof sketches arguing that rooted weak bisimulation equivalence is indeed weak bisimulation congruence typically make some cardinally assumptions, such as that there is an infinite alphabet of actions of which each process uses only a finite subset. The current contribution establishes the validity of this characterisation without making such assumptions. It also argues that the root condition that turns weak bisimulation into rooted weak bisimulation embodies two properties, one of which is needed to obtain a congruence for the +, and one to obtain a congruence for the left-merge.

1 Process Graphs

Definition 1 ([BK86]). A process graph over an alphabet of actions Act is a rooted, directed graph whose edges are labelled by elements of Act. Formally, a process graph g is a triple (nodes(g), root(g), edges(g)), where

– nodes(g) is a set, of which the elements are called the nodes or states of g,

– root(g) ∈ nodes(g) is a special node: the root or initial state of g,

– and edges(g) ⊆ nodes(g) × Act × nodes(g) is a set of triples (s, a, t) with s, t ∈ nodes(g) and a ∈ Act: the edges or transitions of g.

Normally, one is not interested in the names of the nodes in a process graph. For this reason, process graphs are considered up to isomorphism.

Definition 2. Let g and h be process graphs. A graph isomorphism between g and h is a bijective function f : nodes(g) → nodes(h) satisfying

– f(root(g)) = root(h) and

– (s, a, t) ∈ edges(g) ⇔ (f(s), a, f(t)) ∈ edges(h).

Graphs g and h are isomorphic, notation g ≅ h, if there exists a graph isomorphism between them.

If g ≅ h then g and h differ only in the identity of their nodes. Graph isomorphism is an equivalence relation on the class of process graphs.

Further on, process graphs are pictured by using open dots (∘) to denote nodes, and labelled arrows to denote edges. The root is represented by an incoming arrow, not originating from another node. These drawings present process graphs only up to isomorphism.

Let ^{|}G(Act) be the class of process graphs over the alphabet of actions Act up to isomorphism. This means that I am satisfied with a level of precision in describing elements of ^{|}G(Act) that fails to distinguish isomorphic process graphs. In the digression below I will indicate how to raise the precision of my definitions to a fully formal level; the digression should also make clear that it is not really worthwhile to maintain this level throughout the paper.

Next I define the most basic process algebraic operations on ^{|}G(Act): a constant 0 for inaction, a binary infix written operator + for alternative composition or choice, and unary operators a. for action prefixing for each a ∈ Act. For the sake of convenience, in the definition below I will only consider root-acyclic process graphs. In Sect. 3 I will extend the definition to arbitrary process graphs.

Definition 3 ([BK86]). A process graph is root-acyclic if it has no incoming edges at the root. Let ^{|}G^{ρ}(Act) be the class of root-acyclic process graphs over Act up to isomorphism. The constant 0 and the operators a. and +_{ρ} are defined on ^{|}G^{ρ}(Act) as follows. (The subscript ρ serves to distinguish this alternative composition from the more general one that will be defined in Sect. 3.)

– 0 is interpreted as the trivial graph, having one node (the root) and no edges;

– a.g is obtained from g by adding a new node, which will be the root of a.g, and a new a-labelled edge from the root of a.g to the root of g;

– g +_{ρ} h is obtained by identifying the root nodes of disjoint copies of g and h.

Digression: Distinguishing Isomorphic Process Graphs

In Def. 3 I have not bothered to tell which node exactly will be the only node of the process graph 0 and which new node will be added in the construction of a.g. Moreover, in taking the disjoint union of g and h, no explicit solution is offered for what to do when g and h have nodes in common. Here I provide two possible answers. As it doesn’t matter at all which one is chosen, the reader may pick himself, or make up a third.

Making arbitrary choices to resolve ambiguity.

The definitions of 0 and a.g could for instance be given as follows:

– nodes(0) = {∗},

– root(0) = ∗,

– edges(0) = ∅.

– nodes(a.g) = {∗} ∪ {s′ | s ∈ nodes(g)},

– root(a.g) = ∗,

– edges(a.g) = {(∗, a, root(g)′)} ∪ {(s′, a, t′) | (s, a, t) ∈ edges(g)}.

Here the nodes of g are renamed from s into s′, so as to make sure that none of them happens to be the symbol ∗ that is used to name the new root node.

Working modulo isomorphism.

In this approach ^{|}G(Act) is the class of process graph modulo isomorphism, meaning that the elements of ^{|}G(Act) are isomorphism classes of process graphs.

Now 0 ∈ ^{|}G^{ρ}(Act) is defined as the isomorphism class of all trivial process graphs, after observing that all trivial graphs are isomorphic. To obtain the isomorphism class a.G, for G an isomorphism class of process graphs, I first pick a representative g ∈G and a fresh object r ∉ nodes(g). Then a.g is defined by

– nodes(a.g) = nodes(g) ∪ {r},

– root(a.g) = r and

– edges(a.g) = edges(g) ∪ {(r, a, root(g))}.

Finally, a.G is defined to be the isomorphism class containing a.g, and the exercise is concluded by showing that the result is independent of the choice of g ∈ G. Likewise, G +_{ρ} H, for G, H ∈ ^{|}G^{ρ}(Act), is obtained as the isomorphism class of g +_{ρ} h, where g ∈ G and h ∈ H are chosen in such a way that nodes(g) ∩ nodes(h) = root(g) = root(h), and g +_{ρ} h is defined by

– nodes(g +_{ρ} h) = nodes(g) ∪ nodes(h),

– root(g +_{ρ} h) = root(g) = root(h) and

– edges(g +_{ρ} h) = edges(g) ∪ edges(h).

Again, it must be shown that the result is independent of the choice of g and h.

2 Bisimulation Semantics

To make process graphs into a useful semantic model of calculi that enable system verification, a semantic equivalence coarser than isomorphism needs to be defined. The most popular choices are strong and weak bisimulation equivalence, and some of their variants. Such an equivalence can be used fruitfully when it is a congruence for the process algebraic operators that are considered in a particular application. These almost always include the operators 0, a. and +. A semantic equivalence ∼ is a congruence for these operators if g ∼ h implies a.g ∼ a.h and g_{1} ∼ h_{1} ∧ g_{2} ∼ h_{2} implies g_{1} + g_{2} ∼ h_{1} + h_{2}.

2.1 Strong Bisimulation

Definition 4. Let g, h ∈ ^{|}G(Act). The graphs g and h are (strong) bisimulation equivalent, notation g \underline{↔} h, if there exists a binary relation R ⊆ nodes(g) × nodes(h), called a bisimulation between g and h, satisfying, for all a∈Act:

– root(g) R root(h).

– If sRt and (s, a, s′) ∈ edges(g), then ∃(t, a, t′) ∈ edges(h) such that s′Rt′.

– If sRt and (t, a, t′) ∈ edges(h), then ∃(s, a, s′) ∈ edges(g) such that s′Rt′.

It is well-known and easy to check that \underline{↔} is an equivalence relation indeed. I will now show that it is a congruence relation for a. and +_{ρ}. Because these operators have so-far not been defined outside ^{|}G^{ρ}(Act), for now this result will pertain to root-acyclic process graphs only.

Definition 5. A relation between the nodes of two root-acyclic process graphs is called rooted if it relates root nodes with root nodes only.

Lemma 1. Let g, h ∈ ^{|}G^{ρ}(Act). If g \underline{↔} h then there exist a rooted bisimulation between g and h.

Proof. Let R be a bisimulation between g and h. A rooted bisimulation is obtained from R by omitting all liaisons between root nodes and non-root nodes.

Proposition 1. On ^{|}G^{ρ}(Act), bisimulation equivalence is a congruence for a. and +_{ρ}.

Proof. Suppose R is a bisimulation between g and h. Then

R ∪ {(root(a.g), root(a.h))}

is a bisimulation between a.g and a.h. Moreover, invoking Lemma 1, let R_{i} be a rooted bisimulation between g_{i} and h_{i} for g_{i}, h_{i} ∈ ^{|}G^{ρ}(Act) and i = 1, 2 then R_{1} ∪ R_{2} is a bisimulation between g_{1} +_{ρ} g_{2} and h_{1} +_{ρ} h_{2}. ⊓ ⊔ 2.2 Weak Bisimulation

Let τ ∈ Act be the invisible action or silent step. Henceforth, write s ⟶^{a}_{g} s′ for (s, a, s′) ∈ edges(g) and s ⟹_{g} s′ when there are s_{0}, …, s_{n} in nodes(g) such that s = s_{0} ⟶^{τ}_{g} s_{1} ⟶^{τ}_{g} ⋯ ⟶^{τ}_{g} s_{n} = s′. Moreover, s \underrightarrow{a}_{g} s′ denotes that there are nodes s_{1} and s_{2} in g such that s ⟹_{g} s_{1} ⟶^{a}_{g} s_{2} ⟹_{g} s′ and s \underrightarrow{(a)}_{g} s′ is a shorthand for s ⟹_{g} s′ when a = τ, and s \underrightarrow{a}_{g} s′ when a ≠ τ. Thus, s \underrightarrow{(τ)}_{g} s′ says that in g one can travel from s to s′ by performing a sequence of zero or more τ-steps, whereas s \underrightarrow{τ}_{g} s′ requires at least one τ-step. For a ≠ τ there is no difference between \underrightarrow{(a)}_{g} and \underrightarrow{a}_{g}.

Definition 6. Let g, h ∈ ^{|}G(Act). The graphs g and h are weak bisimulation equivalent, notation g \underline{↔}_{w} h, if there exists a binary relation R ⊆ nodes(g) × nodes(h), called a weak bisimulation between g and h, satisfying, for all a∈Act:

– root(g) R root(h).

– If sRt and s ⟶^{a}_{g} s′, then there is a t′ such that t \underrightarrow{(a)}_{h} t′ and s′Rt′.

– If sRt and t ⟶^{a}_{g} t′, then there is an s′ such that s \underrightarrow{(a)}_{h} s′ and s′Rt′.

It is well-known and easy to check that \underline{↔}_{w} is an equivalence relation indeed. However, \underline{↔}_{w} fails to be a congruence for the +. Namely, τ.a.0 \underline{↔}_{w} a.0 but τ.a.0 +_{ρ} b.0 \underline{↮}_{w} a.0 +_{ρ} b.0. The proof of Prop. 1 does not generalise to \underline{↔}_{w} because Lemma 1 does not hold for \underline{↔}_{w}: there is no rooted weak bisimulation between τ.a.0 and a.0.

2.3 Rooted Weak Bisimulation

Although weak bisimulation equivalence captures the invisible nature of the silent step rather well, in order to obtain a congruence, a finer equivalence relation is needed. Such an equivalence was proposed by Bergstra & Klop in [BK85]. In fact it is the obvious “fix” in the definition of weak bisimulation equivalence needed to inherit the proof of Prop. 1.

Definition 7 ([BK85]). Two graphs g, h ∈ ^{|}G^{ρ}(Act) are rooted weak bisimulation equivalent, notation g \underline{↔}_{rw} h, if there exists a rooted weak bisimulation between them (recall Def. 5).

Again, it is easy to check that \underline{↔}_{rw} is an equivalence relation. By definition it is finer than \underline{↔}_{w}. It is strictly finer because τ.0 \underline{↔}_{w} 0 but τ.0 \underline{↮}_{rw} 0 (and likewise τ.a.0\underline{↔}_{w} a.0 but τ.a.0 \underline{↮}_{rw} a.0). Moreover, Lemma 1 implies that \underline{↔}_{rw} is coarser than \underline{↔}. It is strictly coarser because τ.τ.0\underline{↔}_{rw} τ.0 but τ.τ.0 \underline{↮} τ.0.

Proposition 2. On ^{|}G^{ρ}(Act), rooted weak bisimulation equivalence is a congruence for a. and +_{ρ}.

Proof. Suppose R is a rooted weak bisimulation between g and h. Then

R ∪ {(root(a.g), root(a.h))}

is a rooted weak bisimulation between a.g and a.h. Moreover, let R_{i} be a rooted weak bisimulation between g_{i} and h_{i} for g_{i}, h_{i} ∈ ^{|}G^{ρ}(Act) and i = 1, 2 then R_{1} ∪ R_{2} is a rooted weak bisimulation between g_{1} +_{ρ} g_{2} and h_{1} +_{ρ} h_{2}. ⊓ ⊔

3 Root Unwinding

In this section I will generalise the definitions and results of Sections 1 and 2 from root-acyclic to general process graphs.

3.1 The Definition of Alternative Composition

The definition of 0 and a. on ^{|}G(Act) is exactly as on ^{|}G^{ρ}(Act) (see Def. 3). However, defining the + on ^{|}G(Act) as in Def. 3 would yield counterintuitive results. Namely we would have g + h = m, as in the top row of Fig. 1. However, m is able to first do a number of a-actions from g and then a b from h; this is inconsistent with the idea that g + h should from the initial state onwards behave either as g or as h. In fact, strong bisimulation equivalence would fail to be a congruence for this definition of +, for g \underline{↔} g^{ρ}, yet m \underline{↮} k.

a g  +  h  b  ≠  a m  b a a g^{ρ}  +  h  b  =  a a k  b

Fig. 1. Alternative composition of process graphs

For most applications we are interested in process graphs only up to strong bisimulation equivalence. Up to strong bisimilarity, the definition of the + on |G(Act) is completely determined by its definition on ^{|}G^{ρ}(Act), because every process graph is strongly bisimilar with a root-acyclic process graph. The following construction is used to establish this.

Definition 8 ([BK86]). Root unwinding is the operator ρ on ^{|}G(Act) given by

– nodes(ρ(g)) = nodes(g) ._{∪} {∗},

– root(ρ(g)) = {∗} and

– edges(ρ(g)) = edges(g) ∪ {(∗, a, s) | (root(g), a, s) ∈ edges(g)}.

Note that ρ(g) ∈ ^{|}G^{ρ}(Act) for all g ∈ ^{|}G(Act).

Proposition 3 ([BK86]). g \underline{↔} ρ(g) for every process graph g ∈ ^{|}G(Act).

Proof. The relation {(s, s) | s ∈ nodes(g)} ∪ {(root(g), ∗)} is a bisimulation between g and ρ(g). ⊓ ⊔ Definition 9 ([BK86]). The definition of the + is extended from ^{|}G^{ρ}(Act) to |G(Act) by g + h := ρ(g) +_{ρ} ρ(h), where +_{ρ} is given by Def. 3.

This construction automatically entails that \underline{↔} is a congruence for the +.

Proposition 4. On ^{|}G(Act), \underline{↔} is a congruence for a. and +.

Proof. The case of a. goes exactly as in Prop. 1. Let g \underline{↔} g′ and h\underline{↔} h′. Then ρ(g)\underline{↔} g \underline{↔} g′ \underline{↔} ρ(g′) and likewise ρ(h)\underline{↔} ρ(h′). Hence g + h = ρ(g) +_{ρ} ρ(h)\underline{↔} ρ(g′) +_{ρ} ρ(h′) = g′ + h′ by Prop. 1. ⊓ ⊔

On ^{|}G^{ρ}(Act) it is in general not the case that g + h ≅ g +_{ρ} h. However, up to strong bisimilarity, both versions of the + agree.

Proposition 5. Let g, h ∈ ^{|}G^{ρ}(Act). Then g + h \underline{↔} g +_{ρ} h.

Proof. g + h = ρ(g) +_{ρ} ρ(h)\underline{↔} g +_{ρ} h, using Propositions 3 and 1. ⊓ ⊔

It is also possible to merge the definitions of +, +_{ρ} and root unwinding:

Definition 10. Let g, h ∈ ^{|}G^{ρ}(Act). Then g + h can alternatively be defined by

– nodes(g + h) = nodes(g) ._{∪} nodes(h) ._{∪} {∗},

– root(g + h) = {∗} and

– edges(g + h) = edges(g) ∪ edges(h) ∪ {(∗, a, s) | (root(g), a, s) ∈ nodes(g) ∨ (root(h), a, s) ∈ nodes(h)}.

It is trivial to check that up to isomorphism this definition yields the same alternative composition operator as Def. 9.

3.2 Rooted Weak Bisimulation

Postulating that rooted weak bisimulation has to be a coarser equivalence than strong bisimulation, Prop. 3 implies that there is a unique extension of \underline{↔}_{rw} from ^{|}G^{ρ}(Act) to ^{|}G(Act).

Definition 11. Let g, h ∈ ^{|}G(Act). Then g \underline{↔}_{rw} h iff ρ(g)\underline{↔}_{rw} ρ(h) as per Def. 7.

Proposition 6. On ^{|}G(Act), \underline{↔}_{rw} is a congruence for a. and +.

Proof. The case of a. goes exactly as in Prop. 2. Let g \underline{↔}_{rw} g′ and h\underline{↔}_{rw} h′. Then ρ(g)\underline{↔} g \underline{↔}_{rw} g′ \underline{↔} ρ(g′), so ρ(g)\underline{↔}_{rw} ρ(g′), and likewise ρ(h)\underline{↔}_{rw} ρ(h′). Hence g + h = ρ(g) +_{ρ} ρ(h)\underline{↔}_{rw} ρ(g′) +_{ρ} ρ(h′) = g′ + h′ by Prop. 2. ⊓ ⊔

The following characterisation of rooted weak bisimulation equivalence was taken as definition in [Mil90]. Let, for g ∈ ^{|}G(Act) and s ∈ nodes(g), g_{s} denote the process graph obtained from g by appointing s as its root.

Proposition 7. Let g, h ∈ ^{|}G(Act). Then g \underline{↔}_{rw} h iff

– if root(g) ⟶^{a}_{g} s then there is a t such that root(h) \underrightarrow{a}_{h} t and g_{s} \underline{↔}_{w} h_{t};

– if root(h) ⟶^{a}_{h} t then there is an s such that root(g) \underrightarrow{a}_{g} s and g_{s} \underline{↔}_{w} h_{t}.

Proof. “If”: Let B = \{(s, t) ∈ nodes(g) × nodes(h) | g_{s} \underline{↔}_{w} h_{t}\} and

B^{ρ} = B ._{∪} {(root(ρ(g)), root(ρ(h)))} ⊆ nodes(ρ(g)) × nodes(ρ(h)),

recalling that nodes(ρ(g)) = nodes(g) ._{∪} {root(ρ(g))}, and likewise for ρ(h). Assume that both clause above hold. It suffices to show that B^{ρ} is a rooted weak bisimulation between ρ(g) and ρ(h), for by Def. 11 this implies g \underline{↔}_{rw} h. The relation B^{ρ} is rooted by construction. So I need to show it is a weak bisimulation.

Let sB^{ρ}t and s ⟶^{a}_{ρ(g)} s′. It suffices to show that there is a t′ such that t \underrightarrow{(a)}_{ρ(h)} t′ and s′B^{ρ}t′. The other requirement then follows by symmetry.

First assume sBt. In that case, s ⟶^{a}_{g} s′ and g_{s} \underline{↔}_{w} h_{t}, so there is a weak bisimulation R between g_{s} and h_{s}. Thus sRt, and there must be a t′ such that t \underrightarrow{(a)}_{h} t′ and s′Rt′. Hence g_{s′} \underline{↔}_{w} h_{t′}, s′Bt′ and s′B^{ρ}t′. Def. 8 yields t \underrightarrow{(a)}_{ρ(h)} t′.

Now assume s = root(ρ(g)) and t = root(ρ(h)), so root(ρ(g)) ⟶^{a}_{ρ(g)} s′. Then, by Def. 8, root(g) ⟶^{a}_{g} s′, so by the first clause of Prop. 7 there is a t′ such that root(h) \underrightarrow{a}_{h} t′ and g_{s′} \underline{↔}_{w} h_{t′}. Hence s′Bt′ and s′B^{ρ}t′. Def. 8 yields root(ρ(h)) \underrightarrow{a}_{ρ(h)} t′, hence t = root(ρ(h)) \underrightarrow{(a)}_{ρ(h)} t′.

“Only if”: Let R be a rooted weak bisimulation between ρ(g) and ρ(h). Suppose root(g) ⟶^{a}_{g} s. Def. 8 yields root(ρ(g)) ⟶^{a}_{ρ(g)} s, so there must be a t such that root(ρ(h)) \underrightarrow{(a)}_{ρ(h)} t and sRt. As R is rooted, the case that a = τ and t=root(ρ(h)) cannot apply, so root(ρ(h)) \underrightarrow{a}_{ρ(h)} t, hence root(h) \underrightarrow{a}_{h} t by Def. 8. Furthermore, sRt implies g_{s} \underline{↔}_{w} h_{t}. The other clause follows by symmetry.

4 Weak Bisimulation Congruence

A different modification of weak bisimulation equivalence into a congruence for the + was proposed in [HM85].

Proposition 8. For every equivalence relation ∼ on ^{|}G(Act) and every set L of operators on ^{|}G there is a coarsest congruence relation ∼^{c} that is finer than ∼.

Proof. Let a semantic context C[·] be an expression build from process graphs g ∈ ^{|}G(Act) and the hole [·] through application of operators from L, and in which the hole occurs exactly once. If C[·] is a semantic context and g ∈ ^{|}G(Act), then C[g] denotes the process graph obtained by evaluating the expression C[·] in which g is substituted for the hole [·].

Alternatively, a semantic context can be regarded as a unary operator on process graphs: a primitive context is obtained from an operator in L by instantiating all but one of its arguments by process graphs; and a general semantic context is the composition of any number (possibly 0) of primitive contexts.

An equivalence relation ≈ on ^{|}G(Act) is a congruence for L iff for every n-ary operator f in L one has g_{1} ≈ h_{1} ∧⋯∧g_{n} ≈ h_{n} ⇒ f(g_{1}, …, g_{n}) ≈ f(h_{1}, …, h_{n}). This is the case iff for every semantic context C[·] one has g ≈ h ⇒ C[g] ≈ C[h].

Given an equivalence relation ∼ on ^{|}G(Act), define ∼^{c} by

g ∼^{c} h iff C[g] ∼ C[h] for every semantic context C[·].

By construction, ∼^{c} is a congruence on ^{|}G(Act). For if g ∼^{c} h and D[·] is a semantic context, then for every semantic context C[·] also C[D[·]] is a semantic context, so ∀C[·](C[D[g]] ∼ C[D[h]]) and hence D[g] ∼^{c} D[h].

The trivial context guarantees that g ∼^{c} h ⇒ g ∼ h, so ∼^{c} is finer than ∼. Finally, ∼^{c} is the coarsest congruence finer than ∼, because if ≈ is any

congruence finer than ∼, then

g ≈ h ⇒ ∀C[·](C[g] ≈ C[h]) ⇒ ∀C[·](C[g] ∼ C[h]) ⇒ g ∼^{c} h. ⊓ ⊔

Definition 12. The coarsest congruence w.r.t. the + that is finer than weak bisimulation equivalence is called weak bisimulation congruence, notation \underline{↔}_{w}^{c}.

Here I address the question whether both approaches coincide, i.e. whether \underline{↔}_{rw} = \underline{↔}_{w}^{c}. Prop. 6 immediately yields \underline{↔}_{rw} ⊆ \underline{↔}_{w}^{c}. The following proof sketch, due to Jan Willem Klop [personal communication], is a first attempt to establish the reverse.

Proof Sketch. It suffices to restrict attention to the graphs in ^{|}G^{ρ}(Act), for when g \underline{↔}_{w}^{c} h ⇒ g \underline{↔}_{rw} h for g, h ∈ ^{|}G^{ρ}(Act), then by Prop. 3 the same holds for g, h ∈ ^{|}G(Act). [Namely g \underline{↔}_{w}^{c} h ⇒ ρ(g) \underline{↔} g \underline{↔}_{w}^{c} h \underline{↔} ρ(h) ⇒ ρ(g) \underline{↔}_{w}^{c} ρ(h) ⇒ ρ(g)\underline{↔}_{rw} ρ(h) ⇒ g \underline{↔} ρ(g)\underline{↔}_{rw} ρ(h)\underline{↔} h ⇒ g \underline{↔}_{rw} h.]

So let g, h ∈ ^{|}G^{ρ}(Act) and assume g \underline{↔}_{w}^{c} h. Let a ≠ τ be an action that does not occur in either g or h. Then g + a.0\underline{↔}_{w} h + a.0 by the definition of \underline{↔}_{w}^{c}. Let R be a weak bisimulation between g + a.0 and h + a.0.

Claim. R must be rooted.

Proof of Claim. root(g + a.0) ⟶^{a}_{g+a.0} root(0), so if root(g + a.0) R t then t \underrightarrow{a}_{h+a.0} t′ for some t′ ∈ nodes(h+a.0) with root(0) R t′. This is only possible if t = root(h + a.0). By symmetry, s R root(h + a.0) is only possible if s = root(g + a.0).

Application of Claim. The restriction of R to the nodes of g and h is a rooted weak bisimulation between g and h, showing that g \underline{↔}_{rw} h. ⊓ ⊔

The only weak point in this proof sketch is in the choice of an action a ≠ τ that does not occur in g or h. What if such an action does not exists? Below I present two solutions to this problem.

4.1 The Fresh Atom Principle

The Fresh Atom Principle (FAP) allows us to use fresh actions in proofs. It was invented and named by Jan Willem Klop [personal communication]. In order to justify the use of FAP, one needs to realise that for any choice of a set of actions Act containing τ there exists a class ^{|}G(Act) of process graphs over Act. Likewise a parametrised semantic equivalence ∼ has an incarnation in each of these classes, and I write ∼^{Act} to denote the equivalence ∼ as it exists in ^{|}G(Act). Obviously, ^{|}G(A) ⊆ ^{|}G(B) for sets of actions A ⊆ B. Now say that a parametrised equivalence ∼ satisfies FAP, if, whenever A ⊆ B, ∼^{A} is the restriction of ∼^{B} to |G(A), i.e. if for g, h ∈ ^{|}G(A) ⊆ ^{|}G(B) one has g ∼^{A} h ⇔ g ∼^{B} h. It is immediate from their definitions that \underline{↔}, \underline{↔}_{w}, \underline{↔}_{rw} and most other semantic equivalences defined in the literature satisfy FAP. In fact, satisfying FAP looks like a good sanity check for any meaningful equivalence.

In this spirit, one may want to use, instead of \underline{↔}_{w}^{c}, the coarsest congruence finer than \underline{↔}_{w} that satisfies FAP, notation \underline{↔}_{w}^{fc} . This congruence is obtained by allowing, in the proof of Prop. 8, contexts C that may involve fresh actions.

Theorem 1. \underline{↔}_{w}^{fc} coincides with \underline{↔}_{rw}.

Proof. The proof sketch above applies here. After assuming g \underline{↔}_{w}^{fc} h in ^{|}G(Act), apply FAP to obtain g \underline{↔}_{w}^{fc} h in ^{|}G(Act ._{∪} \{a\}). As in the proof sketch, conclude that g \underline{↔}_{rw} h in ^{|}G(Act ._{∪} \{a\}). Since \underline{↔}_{rw} satisfies FAP this implies that g \underline{↔}_{rw} h in ^{|}G(Act). ⊓ ⊔

4.2 Arbitrary Many Non-bisimilar Processes

Even though we now know that \underline{↔}_{rw} coincides with \underline{↔}_{w}^{fc} and thus is the coarsest sane equivalence contained in \underline{↔}_{w} that is a congruence for the +, the question still remains if also \underline{↔}_{w}^{c} coincides with \underline{↔}_{rw}. In case Act = \{τ\}, this is not the case. For in that case \underline{↔}_{w}, and hence also \underline{↔}_{w}^{c}, is the universal relation, but τ.0 \underline{↮}_{rw} 0. However, as I will show in the following, in all other cases we have in fact that \underline{↔}_{w}^{c} = \underline{↔}_{rw}.

Proposition 9 (Jan Willem Klop). Provided that there is at least one action a ∈ Act − {τ}, for each infinite cardinal κ there are at least κ bisimulation equivalence classes of τ-free process graphs in ^{|}G(Act) with less than κ nodes.

Proof. For each ordinal λ define g_{λ} ∈ ^{|}G(Act) as follows.

– g_{0} := 0,

– g_{λ+1} := g_{λ} + a.g_{λ} and

– for λ a limit ordinal, g_{λ} := ∑_{μ<λ} g_{μ}, meaning that g_{λ} is constructed from all graphs g_{μ} for μ < λ by identifying their root.

Claim 1. root(g_{λ}) ⟶^{a}_{g_{λ}} s ⇔ s = root(g_{μ}) for some μ < λ.

Proof of Claim 1. A straightforward transfinite induction on λ.

Claim 2. If μ < λ then g_{λ} \underline{↮} g_{μ}.

Proof of Claim 2, by transfinite induction on λ: Let μ < λ. By Claim 1 we have root(g_{λ}) ⟶^{a}_{g_{λ}} root(g_{μ}). However, when root(g_{μ}) ⟶^{a}_{g_{μ}} s we have s = root(g_{ρ}) for some ρ < μ, and by induction g_{μ} \underline{↮} g_{ρ}. Thus g_{λ} \underline{↮} g_{μ}.

Claim 3. For infinite λ, |nodes(g_{λ})| = |λ|.

Proof of Claim 3. A straightforward transfinite induction on λ, using that the cardinality of a disjoint union of |λ| sets of cardinality 0 < κ ≤ |λ| is |λ|.

Application of the claims. For each infinite cardinal κ there are κ ordinals λ smaller than κ. Now the proposition follows from Claims 2 and 3. ⊓ ⊔

Theorem 2. Provided that there is an a ∈ Act − {τ}, on ^{|}G(Act) weak bisimulation congruence coincides with rooted weak bisimulation equivalence.

Proof. Following the idea from the earlier proof sketch, let g \underline{↔}_{w}^{c} h with g, h ∈ |G^{ρ}(Act). Let κ be the smallest infinite cardinal, such that g and h have less than κ nodes. So there are less than κ process graphs g_{s} with s ∈ nodes(g) and h_{t} with t ∈ nodes(h). Hence by Prop. 9 there is a τ-free process graph k with |nodes(k)| < κ, such that k \underline{↮} g_{s} and k \underline{↮} h_{t} for any such g_{s} and h_{t}. Now g + a.k \underline{↔}_{w} h + a.k by the definition of \underline{↔}_{w}^{c}. Let R be a weak bisimulation between g + a.k and h + a.k.

Claim 1. The restriction of R to nodes(g) × nodes(h) must be rooted.

Proof of Claim 1. root(g + a.k) ⟶^{a}_{g+a.k} root(k), so if root(g + a.k) R t for some t ∈ nodes(h) − \{root(h)\}, then t \underrightarrow{a}_{h+a.k} t′ for some t′ ∈ nodes(h) with root(k) R t′ and hence k \underline{↔}_{w} h_{t′}. By the definition of k this is impossible. Likewise, it is impossible that s R root(h + a.k) for s ∈ nodes(g) − {root(g)}.

Claim 2. The restriction of R to nodes(g) × nodes(h) is a weak bisimulation.

Proof of Claim 2. Let root(g) ⟶^{b}_{g} s. Then root(g + a.k) ⟶^{b}_{g+a.k} s, so there must be a t ∈ nodes(h + a.k) such that root(h + a.k) \underrightarrow{(b)}_{h+a.k} t and s R t. The possibility that b = a and t = root(k) can not occur, for this would imply g_{s} \underline{↔}_{w} k. The possibility that b = τ and t = root(h + a.k) can not occur by Claim 1. Therefore t ∈ nodes(h) − \{root(h)\} and root(h) \underrightarrow{b}_{h} t. Likewise, root(h) ⟶^{b}_{h} t implies that there is an s ∈ nodes(g) − {root(g)} with root(g) \underrightarrow{b}_{g} s and s R t. It follows that the restriction of R to nodes(g)× nodes(h) is a rooted weak bisimulation between g and h. Hence g \underline{↔}_{rw} h. ⊓ ⊔

Rather than working with arbitrary process graphs, some people prefer to set a bound on the number of nodes. This happens for instance when one insists that ^{|}G(Act) should be set rather than a proper class. That can be achieved by first fixing a set N of potential nodes, and then allowing only process graphs g with nodes(g) ⊆ N. For any infinite cardinal κ let ^{|}G_{κ}(Act) be the class of process graphs over Act with less than κ nodes. In particular ^{|}G_{ℵ_{0}}(Act) is the class of regular, or finite-state, process graphs. Theorem 2 transfers smoothly from ^{|}G(Act) to ^{|}G_{κ}(Act).

Theorem 3. Provided that there is an a ∈ Act − {τ}, on ^{|}G_{κ}(Act) weak bisimulation congruence coincides with rooted weak bisimulation equivalence.

Proof. The proof above goes through because the process k fits in ^{|}G_{κ}(Act). ⊓ ⊔ Another cardinality restriction that is sometimes imposed, is the requirement that each node should have less than κ outgoing edges. In case κ > ℵ_{0}, this class of κ-branching process graphs is not essentially different from ^{|}G_{κ}(Act), and the same proof applies. More interesting is the case κ = ℵ_{0}. Up to strong bisimulation equivalence, the finitely branching process graphs form a proper superclass of ^{|}G_{ℵ_{0}}(Act), the finite-state process graphs, and a proper subclass of |G_{ℵ_{1}}(Act), the countable state process graphs. However, as shown in [BBK87], any countable state process graph is weakly bisimilar to a finitely branching process graph. Using this, the proof of Theorem 2 can be adapted to apply to the class of finitely branching process graphs as well.

5 The Left-merge and Rooted Weak Simulations

In [BK85] is has been shown that \underline{↔}_{rw} is a congruence for all operators of ACP_{τ}. Just as for the +, the root condition comes to the rescue in the congruence proof for the left-merge ∥−. One has τ.a.0∥−b.0 \underline{↮}_{w} a.0∥−b.0, because only the former process can do a b before an a, so \underline{↔}_{w} fails to be a congruence for this operator. The reason that the root condition (Def. 5) helps here, is that in g∥−h steps from h can happen in any state of g except the initial one; thus only a weak bisimulation between g_{1} and g_{2} that does not relate roots with non-roots can be modified into a weak bisimulation between g_{1}∥−h and g_{2}∥−h.

There is a directional difference in the way the root condition solves the congruence problems for + and ∥−. This can be seen by applying it to weak simulation.

Definition 13. Let g, h ∈ ^{|}G^{ρ}(Act). The graph g is weakly simulated by the graph h if there exists a binary relation R ⊆ nodes(g) × nodes(h), called a weak simulation from g to h, satisfying, for all a∈Act:

– root(g) R root(h).

– If sRt and s ⟶^{a}_{g} s′, then there is a t′ such that t \underrightarrow{(a)}_{h} t′ and s′Rt′.

A weak simulation from g to h is source rooted if s R root(h) ⇒ s = root(g). It is target rooted if root(g) R t ⇒ t = root(h).

The relation of “being weakly simulation by” is a preorder (transitive and reflexive), called the weak simulation preorder. Likewise one obtains the source rooted weak simulation preorder and the target rooted weak simulation preorder.

Proposition 10. The target rooted weak simulation preorder is a precongruence for the +. This means that if there are target rooted weak simulations from g_{1} to h_{1} and from g_{2} to h_{2}, then there is a target rooted weak simulation from g_{1} + g_{2} to h_{1} + h_{2}.

Proof. Suppose that R_{i} is a target rooted weak simulation from g_{i} to h_{i} for g_{i}, h_{i} ∈ ^{|}G^{ρ}(Act) and i = 1, 2 then R_{1} ∪ R_{2} is a target rooted weak simulation from g_{1} +_{ρ} g_{2} to h_{1} +_{ρ} h_{2}. ⊓ ⊔ Lemma 2. If there is a weak simulation from g to h then there is a target rooted weak simulation from g to h.

Proof. Omit all liaisons of the form root(g) R t with t ≠ root(h). ⊓ ⊔

Corollary 1. The weak simulation preorder is a precongruence for the +, as well as for action prefixing, even without upgrading it with root conditions.

A complete axiomatisation of this preorder is given by the usual axioms for strong bisimulation, together with the axioms x ⊑ x + y and τ.x = x, where the latter is a shorthand for τ.x ⊑ x ∧ x ⊑ τ.x.

Proposition 11. The source rooted simulation preorder is a precongruence for the ∥−.

Proof Idea. Suppose that R is a weak simulation from g to h for g, h ∈ ^{|}G^{ρ}(Act). When adapting R to a weak simulation from g∥−k to h∥−k, one needs to make sure that when g∥−k can do a step from k, then so can h∥−k. The only way this can fail is when a non-root state from g is related to the root of h. In that case g∥−k can do a step from k, but h∥−k cannot. ⊓ ⊔

The weak simulation preorder fails to be a precongruence for the ∥−, for τ.a.0 is weakly simulated by a.0, but τ.a.0∥−b.0 is not weakly simulated by a.0∥−b.0. This is because the weak simulation from τ.a.0 to a.0 is not source rooted. It follows that the source rooted weak simulation preorder is strictly finer than the (target rooted) weak simulation preorder.

It is possible to upgrade the notion of weak simulation by various conditions, such as the following stability requirement [Gla93].

Definition 14. A weak simulation R from g to h is stability respecting if

– if sRt and s −̸→^{τ}_{g} then there is a t′ such that t ⟹_{h} t′ −̸→^{τ}_{h} and sRt′.

Again, target rootedness is needed to make the induced preorder into a precongruence for the +, and source rootedness to make it into a precongruence for the ∥−. This time the two rooted variants are incomparable, because there is a target rooted, but not source rooted, stability respecting weak simulation from τ.a.0 to a.0, and a source rooted, but not target rooted, stability respecting weak simulation from a.0 to τ.a.0.

6 Concluding Remark

The method to turn simulation or bisimulation based equivalences into congruences by insisting on root conditions generalises smoothly to other notions of (bi-)simulation. In the case of branching, delay and η-bisimulation, this is elaborated in [GW96]. Interestingly, the alternative characterisation of rooted weak bisimulation presented in Prop. 7 takes a rather different shape when applied to rooted branching bisimulation. However, the characterisation with the root condition of Def. 5 remains the same.

Acknowledgement. Many crucial ideas incorporated in this paper originate from Jan Willem Klop, and stem from the mid eighties. Originally, Jan Willem and I planned to write a joint pamphlet on this matter, but as this plan never materialised, I finally collected the material in this paper, dedicated to Jan Willem at the occasion of his sixtieth birthday.

References

[BBK87] J.C.M. Baeten, J.A. Bergstra & J.W. Klop (1987): On the consistency of Koomen’s fair abstraction rule. Theoretical Computer Science 51(1/2), pp. 129–176.

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

[BK86] J.A. Bergstra & J.W. Klop (1986): Algebra of communicating processes. In J.W. de Bakker, M. Hazewinkel & J.K. Lenstra, editors: Mathematics and Computer Science, CWI Monograph 1, North-Holland, pp. 89–138.

[Gla93] R.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 CONCUR’93, 4^{th} International Conference on Concurrency Theory, Hildesheim, Germany, LNCS 715, Springer, pp. 66–81.

[GW96] R.J. van Glabbeek & W.P. Weijland (1996): Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), pp. 555–600.

[HM85] M. Hennessy & R. Milner (1985): Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1), pp. 137–161.

[Mil90] 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.