next up previous
Next: Branching and Abstraction Up: Branching Time and Abstraction Previous: Branching Time and Abstraction

Introduction

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.

A paper by JONSSON & PARROW (1993) on deciding bisimulation equivalence shows a different kind of struggle with the third t-law. In this paper, infinite data flow is turned into a finite state representation by considering symbolic transitions. This provides us with a method to decide on the equivalence of infinite data flow programs. It turns out to work easily for strong equivalence, but for observation equivalence there is no straightforward generalization of the former results and a less intuitive transition system is needed to fix this problem. It is easy to see that using branching bisimulation would serve as a key to a more natural solution of this problem.

Having at least four options for the definition of bisimulation congruence involving t-steps, in any particular application it becomes important to have a clear intuition about which kind of abstraction is preferable. In an important class of problems one can prove however, that all four notions of bisimulation yield the same equivalence. In particular this is the case if one of the two bisimulating graphs does not have any t-steps. It is interesting to observe that, as far as we know, all case studies on protocol verification performed so far fit into this class of problems, hence all of their proofs that have been given in the setting of observation equivalence still hold in branching bisimulation semantics.



next up previous
Next: Branching and Abstraction Up: Branching Time and Abstraction Previous: Branching Time and Abstraction

Rob van Glabbeek