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:
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:
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.*
--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.
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:
PROOF First we prove Lemma 1.1 for a slightly different kind of bisimulation, defined as follows:
The difference with branching bisimulation is the first case of (2), which can be illustrated by:
v--t->v' v--t->v' | /| | / | / | | / | / | | / | / | | / |/ | |/ w ==> w' wFigure 3. Semi branching (left) and branching bisimulation.
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 * {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
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.