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:
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:
Now let us postulate the existence of a special action
t 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:
DEFINITION 1.3 Two graphs g and h are weakly bisimilar -- notation: g =w
h -- if there exists a symmetric relation R (called a weak bisimulation)
between the nodes of g and h such that:
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: 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.*
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:
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:
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:
So assume not R(v,w), then we find that either (1) v=s and
w=ri or (2) v=ri and w=s.
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:
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 *
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
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.
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.
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.
Again, =w is an equivalence on G which is called weak (bisimulation)
equivalence, also known as observation equivalence or
t-bisimulation equivalence.
Although less
useful for purposes of verification, in this (original) form the weak
bisimulation shows a clear parallel with the
t-less version.
--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.
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.
CLAIM The largest semi branching bisimulation between g and h
satisfies (*).
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
This proves that R' is a semi branching bisimulation. Since R
is the largest we find R=R'.
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:
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.
{w,h,d}, =* is an equivalence relation on G.
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
Next: From Equivalence to