5.2.2.2 Diamond elimination

This procedure assumes that the relation of -reachibility is a partial order on nodes. If the input transition system is known to be divergence free then this is true, otherwise -loop elimination is required first (since this procedure guarantees to achieve the desired state).

Under this assumption, diamond reduction can be described as follows, where the input state-machine is S (in which nodes can be marked with information such as minimal acceptances), and we are creating a new state-machine T from all nodes explored in the search:

• Begin a search through the nodes of S starting from its root N₀. At any time there will be a set of unexplored nodes of S; the search is complete when this is empty.
• To explore node N, collect the following information:
  • The set (N) of all nodes reachable from N under a (possibly empty) sequence of actions.
  • Where relevant (based on the equivalence being used), divergence and minimal acceptance information for N: it is divergent if any member of (N) is either marked as divergent or has a to itself. The minimal acceptances are the union of those of the members of (N) with non-minimal sets removed. This information is used to mark N in T.
  • The set V(N) of initial visible actions: the union of the set of all non- actions possible for any member of (N).
  • For each aV(N), the set N_a = N after a of all nodes reachable under a from any member of (N).
  • For each aV(N), the set min(N_a) which is the set of all -minimal elements of N_a (i.e., those nodes not reachable under from any other in N_a).
• A transition (labelled a) is added to T from N to each N' in min(N_a), for all aV(N). Any nodes not already explored are added to the search.

This creates a transition system where there are no -actions but where there can be ambiguous branching under visible actions, and where nodes might be labelled as divergent. The reason why this compresses is that we do not include in the search nodes where there is another node similarly reachable but demonstrably at least as nondeterministic: for if M (N) then N is always at least as nondeterministic as M. The hope is that the completed search will tend to include only those nodes that are -minimal in T. Notice that the behaviours of the nodes not included from N_a are nevertheless taken account of, since their divergences and minimal acceptances are included when some node of min(N_a) is explored.

It seems counter-intuitive that we should work hard not to unwind 's rather than doing so eagerly. The reason why we cannot simply unwind 's as far as possible (i.e., collecting the -maximal points reachable under a given action) is that there will probably be visible actions possible from the unstable nodes we are trying to bypass. It is impossible to guarantee that these actions can be ignored.

The reason we have called this compression diamond elimination is because what it does is to (attempt to) remove nodes based on the diamond-shaped transition arrangement where we have four nodes P, P', Q, Q' and P P', Q Q', P Q and P' Q'. Starting from P, diamond elimination will seek to remove the nodes P' and Q'. The only way in which this might fail is if some further node in the search forces one or both to be considered.

A Lemma in [RosEtAl95] shows that the following two types of node are certain to be included in T:

• The initial node N₀.
• S₀, the set of all -minimal nodes (ones not reachable under from any other).

Let us call S₀ {N₀} the core of S. The obvious criteria for judging whether to try diamond reduction at all, and of how successful it has been once tried, will be based on the core. For since the only nodes we can hope to get rid of are the complement of the core, we might decide not to bother if there are not enough of these as a proportion of the whole. And after carrying out the reduction, we can give a success rating in terms of the percentage of non-core nodes eliminated.

Experimentation over a wide range of example CSP processes has demonstrated that diamond elimination is a highly effective compression technique, with success ratings usually at or close to 100% on most natural systems. To illustrate how diamond elimination works, consider one of the most hackneyed CSP networks: N one-place buffer processes chained together.

COPY COPY ... COPY COPY

Here, COPY=left?x right!x COPY. If the underlying type of (the communications on) channel left (and right) has k members then COPY has k+1 states and the network has (k+1) ^N [k+1 to the power N]. Since all of the internal communications (the movement of data from one COPY to the next) become actions, this is an excellent target for diamond elimination. And in fact we get 100% success: the only nodes retained are those that are not -reachable from any other. These are the ones in which all of the data is as far to the left as it can be: there are no empty COPY's to the left of a full one. If k=1 this means there are now N+1 nodes rather than 2 ^N [2 to the power N], and if k=2 it gives 2 ^N+1 -1 [one less than 2 to the power N+1] rather than 3 ^N [3 to the power N].

Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.