When comparing semantic equivalences for concurrency, it is common
practice to distinguish between *linear time* and *branching time*
equivalences (see for instance DE BAKKER, BERGSTRA, KLOP & MEYER
(1984), PNUELI (1985)). In the former, a process is determined by its
possible executions, whereas in the latter also the branching
structure of processes is taken into account. The standard example of
a linear time equivalence is *trace equivalence* as employed in HOARE
(1980); the standard example of a branching time equivalence is
*observation equivalence* or *bisimulation equivalence* as defined by
MILNER (1980) and PARK (1981) (cf. MILNER (1983), MILNER (1989)).
Between pure linear time and branching time equivalences there are
several *decorated trace equivalences*
(cf. BAETEN, BERGSTRA & KLOP (1987b), BLOOM, ISTRAIL & MEYER (1995),
BROOKES, HOARE & ROSCOE (1984), DE NICOLA & HENNESSY (1984), HOARE
(1985), OLDEROG & HOARE (1986), PHILLIPS (1987), PNUELI (1985),
POMELLO (1986)), preserving part of the branching structure of
processes but for the rest resembling trace equivalence.

Originally, the most popular argument for employing branching
time semantics was the fact that it allows a proper modelling of
*deadlock behaviour*, whereas linear time semantics does not.
However, this advantage is shared with the decorated trace semantics
which have the additional advantage of only distinguishing between
processes that can be told apart by some notion of *observation*
or *testing*. The main criticism on observation equivalence---and
branching time equivalences in general---is that it is not an
observational equivalence in that sense: distinctions between
processes are made that cannot be observed or tested, unless observers
are equipped with extraordinary abilities like that of a copying
facility together with the capability of global testing as in MILNER
(1980,1981) or ABRAMSKY (1987).

Nevertheless, branching time semantics is of fundamental importance in concurrency, exactly because it is independent of the precise nature of observability. Which one of the decorated trace equivalences provides a suitable modelling of observable behaviour depends in great extent on the tools an observer has to test processes. And in general a protocol verification in a particular decorated trace semantics, does not carry over to a setting in which observers are a bit more powerful. On the other hand, branching time semantics preserves the internal branching structure of processes and thus certainly their observable behaviour as far as it can be captured by decorated traces. A protocol verified in branching time semantics is automatically valid in each of the decorated trace semantics.

Probably one of the most important features in process algebra is that
of abstraction, since it provides us with a mechanism to *hide* actions
that are not observable, or not interesting for any other reason. By
abstraction, some of the actions in a process are made *invisible* or
*silent*. Consequently, any consecutive execution of hidden steps
cannot be recognized since we simply do not `see' anything happen.

Algebraically, in ACPt of BERGSTRA & KLOP (1985)
abstraction has the form of a renaming operator which renames actions
into a *silent move* called **t**. In MILNER's CCS (MILNER
(1980)) these silent moves result from synchronization. This new
constant **t** is introduced in the algebraic models as well: for
instance in the *graph models* (cf. BERGSTRA & KLOP (1985), MILNER
(1980)) we find the existence of **t**-edges, and so the question
was how to find a satisfactory extension of the original definition of
*bisimulation equivalence* that we had on process graphs without
**t**.

It turns out that there exist many possibilities for extending
bisimulation equivalence to process graphs with **t**-steps. One such
possible extension is incorporated in Milner's notion of *observation
equivalence*---also called *weak bimulation equivalence*---, which
resembles ordinary bisimulation, but permits arbitrary sequences of
**t**-steps to precede or follow corresponding atomic actions. A different
notion, the so-called *eta bisimulation*, was suggested by BAETEN
& VAN GLABBEEK (1987), yielding a weaker set of abstraction
axioms. In MILNER (1981) another notion of observational equivalence
was introduced which in this paper is referred to as *delay
bisimulation equivalence*. As we will show, the treatments of Milner
and Baeten & Van Glabbeek fit into a natural structure of four
possible variations of bisimulation equivalence involving silent
steps. The structure is completed by defining *branching bisimulation
equivalence*. As it turns out, observation equivalence is the coarsest
equivalence of the four, in the sense of identifying more processes.
Eta and delay bisimulation equivalence are two incomparable finer
notions whereas branching bisimulation equivalence is the finest of
all.

In a certain sense the usual notion of observation equivalence
does not preserve the branching structure of a process.
The processes **a(tb + c)** and **a(tb + c) + ab** for instance are
observation equivalent. However, in the first term, in each
computation the choice between **b** and **c** is made after
the **a**-step, whereas the second term has a computation in which
**b** is already chosen when the **a**-step occurs. For this
reason one may wonder whether or not we should accept the so-called
third **t**-law---**a(tx + y) = a(tx + y) + ax**---that is
responsible for the former equivalence. Similarly, the processes **ta
+ b** and **ta + a + b** are observation equivalent. However,
only in the first term every computation in which **a** occurs passes
through a state where a did not yet happen but the possibility to do **b**
instead is already discarded. Hence we argue that also the second
**t**-law---**tx = tx + x**--- (responsible for the latter
equivalence) does not respect branching time.

These examples show us that while preserving observation
equivalence, we can introduce new paths in a graph that were not there
before. To be precise: the *traces* are the same, but the sequences of
intermediate nodes are different (modulo observation equivalence),
since in the definition of observation equivalence there is no
restriction whatsoever on the nature of the nodes that are passed
through during the execution of a sequence of **t**-steps, preceding or
following corresponding atomic actions. This is the key point in our
definition of branching bisimulation equivalence: in two bisimilar
processes every 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. It turns out that it can be defined by a small change in the
definition of observation equivalence.

The fact that observation equivalence can be too coarse in its
identifications is illustrated even more strongly by the problems that
it may cause in practical applications and analysis. As an example, it can be shown (cf. GRAF &
SIFAKIS (1987)) that there is no modal logic with *eventually*
operator **<>** which is *adequate* for observation
equivalence, in the sense that two processes are observation
equivalent iff they satisfy the same modal formulas. Here **P |=
<>p** means that all paths from process **P** will sooner or
later reach a state were **p** holds. Indeed, suppose that such a
logic *would* exist, then there exists a formula **p** such
that: **(tb + c) |= p** and *not*(**b |= p**) since
obviously these processes are not observation equivalent. However,
from

**(tb + c) |= p** it follows that we have **a(tb + c) |=
<>p** whereas from *not*(**b |= p**) we find
*not*(**a(tb + c) + ab |= <>p**) although both processes are
observation equivalent. Obviously, this inconsistency is due to the
third **t**-law. Similarly there must be a formula **q** such
that **a |= q** and *not*(**ta + a + ba |= q**). Thus **ta
+ ba |= q**, whereas whereas *not*(**ta + a + ba |= <>q**),
although both processes are observation equivalent. This time the
inconsistency is due to the second **t**-law.