not been previously marked as unsolvable, are added to the queue. The goal sets in this queue are considered in order, always for achievement in the buffer layer. Thus, rather than constructing a new layer each time the top level goal set proves unsolvable, and then reconsidering all of the same achievers in the new layer, the goal sets in the queue are simply considered in the buffer layer. We call this mechanism a wave front because it pushes goal sets forward from the fix point layer into the buffer, and then recedes to consider another goal set from the fix point layer. The goal sets generated at the fix point, which join the queue for propagation, are referred to as candidate goal sets. The wave front is depicted in Figure 10. The underlying implementation of the plan graph remains based on the spike, but the figure depicts the graph in the traditional way for simplicity.

In the picture, G represents the top level goal set and when it is used to initiate a plan search from the buffer layer it generates the sequence of goal sets G1, G2 and G3 at the fix point layer. Assuming that these all fail, the first set in this queue, G1, is propagated forward to the buffer leading to the generation of goal sets G4 and G5 in the fix point layer. These are added to the end of the queue and G2 will be the next goal set selected from the queue to propagate forward.

In order to demonstrate that the wave front machinery maintains an appropriate behaviour there are three questions to be considered.

1. Is every goal set that would have been considered in the buffer layer, had the graph been constructed explicitly, still considered using the wave front? This question concerns completeness of the search process.

2. Does every plan generated to achieve a goal set that is considered in the buffer layer correspond to a plan that would have been generated had the graph been explicitly constructed? This question concerns soundness.

3. The final question concerns whether the termination properties of Graphplan are m aintained.
Definition 12 A k-level goal tree for goal set G at layer n in a plan graph, GT k.Gn, is a general tree of depth k in which the nodes are goal sets and the parent-child relationship is defined as follows. If the goal set x is in the tree at level i then the goal set y is a child of x if y is a minimal goal set containing no mutex goal pairs such that achievement of y at layer n - i - 1 in the plan graph enables the achievement of x at layer n - i in that graph.

We take the root to be at level 0 of the tree and the leaves to be at level k - 1.

Lemma 1  If n - k ≥ FP then GT k,G,n = GT k,G,n+1, where FP is the number of the fix point layer in the plan graph.

Proof By definition of the fix point, all layers in a plan graph beyond the fix point contain an exact replica of the information contained at the fix point layer. Since, by definition of the goal tree, the parent-child relationship depends exclusively upon the relationship between two consective layers in the plan graph, and layers cannot change after the fix point, it follows that if x is the parent of y at some layer beyond the fix point then the parent-child relationship between x and y must hold at any pair of consecutive layers beyond the fix point. Further, no new parent-child relationships can arise beyond the fix point. The