   Next: From Equivalence to Up: Branching Time and Abstraction Previous: Introduction

Branching and Abstraction

In this section we define the semantic equivalences that we want to discuss on a domain of process graphs. Since we focus on branching and abstraction, we have chosen to abstain from a proper modelling of divergence, concurrency, real-time behaviour and stochastic aspects of processes. Moreover, we will disregard the nature of the actions that our processes may perform: they will be modelled as uninterpreted symbols a,b,c,... from a given set Act. We have chosen process graphs (or labelled transition systems) to represent processes, since they clearly visualize the aspects of the modelled systems' behaviour we are interested in. The nodes in our graphs (or states in our transition systems) remain anonymous. A common alternative is to use closed expressions in a system description language like CCS or ACP as nodes in process graphs, but here we prefer to separate the semantic issues from the treatment of a particular language. In the next section, however, we will give an interpretation of a subset of CCS in the graph model and discuss the algebraic aspects of our equivalences.

DEFINITION 1.1 A process graph is a connected, rooted, edge-labelled and directed graph.

In an edge-labelled directed graph, edges go from one node to another (or the same) node and are labelled with elements from a certain set Act. One can have more than one edge between two nodes as long as they carry different labels. A rooted graph has one special node which is indicated as the root node. We require process graphs to be connected: they need not be finite, but one must be able to reach every node from the root node by following a finite path. If r and s are nodes in a graph, then r--a->s denotes an edge from r to s with label a or it will be used as a proposition saying that such an edge exists. Process graphs represent concurrent systems in the following way: the elements of Act are actions a system may perform; the nodes of a process graph represent the states of a concurrent system; the root is the initial state and if r--a->s, then the system can evolve from state r to state s by performing an action a. The domain of process graphs will be denoted by G.

On G we consider the notion of bisimulation equivalence, which originally was due to PARK (1981) and used in MILNER (1983, 1985, 1989) and in a different formulation already in MILNER (1980). On the domain of process graphs, a bisimulation usually is defined as a relation R on the nodes of graphs g and h satisfying:

1. The roots of g and h are related by R
2. If R(r,s) and r --a-> r', then there exists a node s' such that s --a-> s' and R(r',s')
3. If R(r,s) and s --a-> s', then there exists a node r' such that r --a-> r' and R(r',s').
Equivalently -- as is done in this paper -- one can obtain bisimulation equivalence from a symmetric relation R between nodes of g and h, only satisfying (i) and (ii). Such a symmetric relation can be defined as a subset R of nodes(g) x nodes(h) U nodes(h) x nodes(g) such that R(r,s) <==> R(s,r), or, alternatively, as a set of unordered pairs of nodes R subset {{r,s} | r nodes(g), s nodes(h). In the latter case R(r,s) abbreviates {r,s} R. Note that a symmetric relation satisfying (i) and (ii) also satisfies (iii). and therefore is a bisimulation as defined above. Furthermore, if R is a bisimulation in the sense defined above, then the union of R and its inverse is a symmetric bisimulation between these graphs. Hence the restriction to symmetric relations does not cause any loss of generality.

DEFINITION 1.2 Two graphs g and h in G are (strongly) bisimilar -- notation: g =s h -- if there exists a symmetric relation R between the nodes of g and h (called a bisimulation) such that:

1. The roots of g and h are related by R
2. If R(r,s) and r --a-> r', then there exists a node s' such that s --a-> s' and R(r',s')
Bisimilarity turns out to be an equivalence relation on G which is called bisimulation equivalence. Depending on the context we will sometimes use Milner's terminology and refer to bisimulation equivalence as strong equivalence or strong congruence.

Now let us postulate the existence of a special action t Act, that represents an unobservable, internal move of a process. We write r ==> s for a path from r to s consisting of an arbitrary number (possibly 0) of t-steps.

The definition of strong congruence was the starting point of MILNER (1980) when he considered abstraction in CCS. Having in mind that t-steps are not observable, he suggested to simply require that for g and h to be equivalent, (i) every possible a-step (a not t) in the one graph should correspond with an a-step in the other (as for usual bisimulation equivalence), apart from some arbitrary long sequences of t-steps that are allowed to precede or follow, and (ii) every t-step should correspond to an arbitrary long (possibly empty) t-sequence. This way he obtained his notion of observation equivalence (cf. MILNER (1980, 1985, 1989)) -- or weak bisimulation equivalence -- which can be defined as follows:

1. The roots are related by R
2. If R(r,s) and r --a-> r', then either a=t and R(r',s), or there exists a path s ==> s1 --a-> s2 ==> s' such that R(r',s').
Again, =w is an equivalence on G which is called weak (bisimulation) equivalence, also known as observation equivalence or t-bisimulation equivalence.

For s=a1a2... a (possibly empty) sequence of visible actions let p ==s=> q denote p ==> --a1-> ==> --a2-> ==> . . . ==> --an-> ==> q, i.e. a path from p to q passing through a sequence of actions that reduces to s after leaving out the internal ones. Then a weak bisimulation can be equivalently defined as a symmetric relation between the nodes of graphs g and h, such that:

1. The roots are related by R
2. If R(r,t) and r ==s=> r', then there exists a path t ==s=> t' such that R(r',t').
Although less useful for purposes of verification, in this (original) form the weak bisimulation shows a clear parallel with the
t-less version.

Still, to some extent, the notion of weak bisimulation cannot be regarded as the natural generalization of ordinary bisimulation to an abstract setting with hidden steps. The reason for this is that an important feature of a bisimulation is missing for weak bisimulation, namely the property that any computation in the one process corresponds to a computation in the other, in such a way that all intermediate states of these computations correspond as well, due to the bisimulation relation. When HENNESSY & MILNER (1980) introduced the first version of observation equivalence, they also insisted on relating the intermediate states of computations, as they tell us: "... any satisfactory comparison of the behaviour of concurrent programs must take into account their intermediate states as they progress through a computation, because differing intermediate states can be exploited in different program contexts to produce different overall behaviour ..." and: "If we consider a computation as a sequence of experiments (or communications), then the above remarks show that the intermediate states are compared. In fact, if p is to be equivalent to q, there must be a strong relationship between their respective intermediate states. At each intermediate stage in the computations, the respective RpotentialsS must also be the same". However, in Milner's observation equivalence, when satisfying the second requirement of Definition 1.3 one may execute arbitrary many t-steps in a graph without worrying about the status of the nodes that are passed through in the meantime.*

--a->*--t->*--b->*--t->*--c->
|     |     |     |
d1    d2    d3    d4
|     |     |     |
V     V     V     V

____b____              (a)              ____b____
/         \                             /         \
|           |                           |           |
|           V                           |           V
--a->*--t->*--b->*--t->*--c->     --a->*--t->*--b->*--t->*--c->
|     |     |     |               |     |     |     |
d1    d2    d3    d4              d1    d2    d3    d4
|     |     |     |               |     |     |     |
V     V     V     V               V     V     V     V

(b)                               (c)
FIGURE 1. Observation equivalence.

As an illustration, in Figure 1 we consider a path atbtc with outgoing edges d1,...,d4, and it follows easily that all three graphs are observation equivalent. Note that one may add extra b-edges as in (b) and (c) without disturbing equivalence. However, in both (b) and (c) a new computation path is introduced -- in which the outgoing edge d2 (or d3 respectively) is missing -- and such a path did not occur in (a). Or -- to put it differently -- in the path introduced in (b) the options d1 and d2 are discarded simultaneously, whereas in (a) it corresponds to a path containing a state where the option d1 is already discarded but d2 is still possible. Also in the path introduced in (c) the choice not to perform d3 is already made with the execution of the b-step, whereas in (a) it corresponds to a path in which this choice is made only after the b-step. Thus we argue that observation equivalence does not preserve the branching structure of processes and hence lacks one of the main characteristics of bisimulation semantics.

Consider the following alternative definition of bisimulation in order to see how this can be overcome.

DEFINITION 1.4 Two graphs g and h are branching bisimilar -- notation: g =b h -- if there exists a symmetric relation R (called a branching bisimulation) between the nodes of g and h such that:

1. The roots are related by R
2. If R(r,s) and r --a-> r', then either a=t and R(r',s), or there exists a path s ==> s1 --a-> s2 ==> s' such that R(r,s1), R(r',s2) and R(r',s').
In a picture, the difference between branching and weak bisimulation can be characterized as follows:
r --a-> r'
/:       :\
/ :       : \
/ (1)     (2) \
R   :       :   R
/    :       :    \
s ==> s1--a-> s2==> s'
FIGURE 2. Bisimulations with t.

Ordinary weak bisimulation says that every a-step r --a-> r' corresponds with a path s ==> s1 --a-> s2 ==> s' and so we obtain Figure 2 without the lines marked with (1) and (2). Branching bisimulation moreover requires relations between r and s1 and between r' and s2 and thus we obtain Figure 2 with (1) and (2). Note that if g =b h then there exists a largest branching bisimulation between g and h, since the set of branching bisimulations is closed under arbitrary union.

Obviously, branching bisimilarity more strongly preserves the branching structure of a graph since the starting and endnodes of the t-paths s ==> s1 and s2 ==> s are related to the same nodes. Observe that in Figure 1 there are no branching bisimulations between any of the graphs (a), (b) and (c). In particular, adding extra edges as in (b) and (c) no longer preserves branching bisimilarity. Equivalently, we could have strengthened Definition 1.3 (ii) by requiring all intermediate nodes in s ==> s1 and s2 ==> s to be related with r and r' respectively. In fact, this would yield the notion we really want to define. That Definition 1.4 yields the same relation can be seen by use of the following lemma:

LEMMA 1.1 (stuttering lemma) Let R be the largest branching bisimulation between g and h. If r --t-> r1 --t-> ... --t-> rm --t-> r' (m > 0) is a path such that R(r,s) and R(r',s) then, for i=1,...,m: R(ri,s).

PROOF First we prove Lemma 1.1 for a slightly different kind of bisimulation, defined as follows:

Now let (*) denote the property, mentioned in the lemma. Observe that (a) any branching bisimulation is a semi branching bisimulation and (b) any semi branching bisimulation satisfying (*) is a branching bisimulation.
CLAIM The largest semi branching bisimulation between g and h satisfies (*).

Let R be the largest semi branching bisimulation between g and h, let s be a node and let r --t-> r1 --t-> ... --t-> rm --t-> r' (m > 0) be a path such that R(r,s) and R(r',s). Then we prove that R' = R U {{ri,s} | i=1,...,m } is a semi branching bisimulation. We check the conditions:

• The root nodes of g and h are related by R', since they are related by R.
• Suppose R'(v,w) and v --a-> v'. If R(v,w) then it follows that either (a) a=t and there exists a path w ==> w' such that R(v,w') and R(v',w'), or (b) there exists a path w ==> w1 --a-> w2 ==> w' such that R(v,w1), R(v',w2) and R(v',w'). Hence, since R' contains R we find that R' satisfies the requirements in the definition above.

So assume not R(v,w), then we find that either (1) v=s and w=ri or (2) v=ri and w=s.

1. If s --a-> s' then it follows from R(r',s) that
• either: a=t and there is a path r' ==> r" such that R(r",s) and R(r",s'). Hence there is a path ri ==> r' ==> r" such that R'(r",s) and R'(r",s') as required.
• or: there is a path r' ==> t1 --a-> t2 ==> r" such that R(t1,s), R(t2,s') and R(r",s') and hence ri ==> r' ==> t1 --a-> t2 ==> r" with R'(t1,s), R'(t2,s') and R'(r",s').
2. If ri --a-> r" then r --t-> r1 --t-> ... --t-> ri --a-> r" and since R(r,s) we find that there exists a sequence s ==> s1 ==> ... ==> si such that R(r1,s1),...,R(ri,si). It follows from R(ri,si) that
• either: a=t and there exists a path si ==> s' such that R(ri,s') and R(r",s'). Hence s ==> s' with R'(ri,s') and R'(r",s') as required.
• or: there exists a path si ==> t1 --a-> t2 ==> s" such that R(ri,t1), R(r",t2) and R(r",s"), and hence s ==> si ==> t1 --a-> t2 ==> s" with R'(ri,t1), R'(r",t2) and R'(r",s").
This proves that R' is a semi branching bisimulation. Since R is the largest we find R=R'.
So we proved the claim. Finally, conclude that the largest semi branching bisimulation is equal to the largest branching bisimulation, and thus we proved the lemma. QED

The stuttering lemma will play a crucial role in some of the results we will present later. An alternative proof can be found in DE NICOLA, MONTANARI & VAANDRAGER (1990).

It follows from Figure 2 that we can find two more kinds of bisimulation with t, since we can leave out (1) while still having (2) and vice versa. Consider the following two definitions:

DEFINITION 1.5 Two graphs g and h are eta-bisimilar -- notation g =h h -- if there exists a symmetric relation R (called an eta-bisimulation) between the nodes of g and h such that:

1. The roots are related by R
2. If R(r,s) and r --a-> r', then either a=t and R(r',s), or there exists a path s ==> s1 --a-> s2 ==> s' such that R(r,s1) and R(r',s').
DEFINITION 1.6 Two graphs g and h are delay bisimilar -- notation g =d h -- if there exists a symmetric relation R (called a delay bisimulation) between the nodes of g and h such that:
1. The roots are related by R
2. If R(r,s) and r --a-> r', then either a=t and R(r',s), or there exists a path s ==> s1 --a-> s2 ==> s' such that R(r',s2) and R(r',s').
Notice the subtle differences between both definitions (and
Definition 1.4). In Definition 1.5 the notion of eta-bisimulation corresponds to Figure 2 without the relation (2) but with (1). Similarly, with delay bisimulation we have (2) but not (1). It is easy to see that in the definition of both branching and delay bisimulation the existence requirement of a node s' such that s2 ==> s' and R(r',s') is redundant.

From the definitions we find immediately that g =b h implies g =h h implies g =w h and similarly g =b h implies g =d h implies g =w h. Observe that in Figure 1 we find an eta-bisimulation between (a) and (c) and a delay bisimulation between (a) and (b). Conversely, there is no h-bisimulation between (a) and (b) and no delay bisimulation between (a) and (c), so all implications are strict.

The notion of eta-bisimulation was first introduced by BAETEN & VAN GLABBEEK (1987) as a finer version of observation equivalence. A variant of delay bisimulation -- only differing in the treatment of divergence -- first appeared in MILNER (1981), also under the name observational equivalence.

PROPOSITION 1.2 For * {w,h,d}, =* is an equivalence relation on G.

PROOF =* is reflexive since the identity relation is a *-bisimulation between any graph and itself, and it is symmetric by definition. Furthermore let R be a *-bisimulation between g and g', and S a *-bisimulation between g' and g". Their composition RoS is defined by

RoS(r,r") iff for some r' in g': R(r,r') and S(r',r").
Now one can easily prove that RoS U SoR is a *-bisimulation between g and g", so =* is transitive. QED

In VAN GLABBEEK & WEIJLAND (1990) we claimed that the proof above would also work for *=b, showing that branching bisimilarity is an equivalence. However, BASTEN (1996) showed that this is not the case, since RoS U SoR need not be a branching bisimulation.

PROPOSITION 1.3 Branching bisimilarity is an equivalence relation on G.

PROOF Reflexivity and symmetry proceed as before. Let R be a branching bisimulation between g and g', and S a branching bisimulation between g' and g". Now one can easily prove that RoS U SoR is a semi branching bisimulation between g and g", which implies that g =b g". Thus =* is transitive. This proof is eleborated in detail in BASTEN (1996).

For an alternative transitivity proof assume g =b g' =b g". Then there exists branching bisimulations R between g and g' and S between g' and g" satisfying the property of Lemma 1.1. Now RoS U SoR is a branching bisimulation between g and g".

A third way to obtain Proposition 1.3 is as an immediate consequence of Theorem 3.3. QED

We therefore refer to =b as branching bisimulation equivalence or branching equivalence for short.   Next: From Equivalence to Up: Branching Time and Abstraction Previous: Introduction

Rob van Glabbeek