In this section, first we describe the basic plan-rewriting algorithm in PbR. Second, we prove this algorithm sound and discuss some formal properties of rewriting. Finally, we discuss a family of algorithms for plan rewriting depending on parameters such as the language for defining plan operators, the specification language for the rewriting rules, and the requirements of the search method.
The plan-rewriting algorithm is shown in Figure 13. The algorithm takes two inputs: a valid plan , and a rewriting rule ) ( is the antecedent query, is the replaced subplan, and is the replacement subplan). The output is a valid rewritten plan . The matching of the antecedent of the rewriting rule () determines if the rule is applicable and identifies the steps and links of interest (line 1). This matching can be seen as subgraph isomorphism between the antecedent subplan and the current plan (with the results then filtered by applying the :constraints). However, we take a different approach. PbR implements rule matching as conjunctive query evaluation. Our implementation keeps a relational representation of the steps and links in the current plan similar to the node and link specifications of the rewriting rules. For example, the database for the plan in Figure 4 contains one table for the unstack steps with schema (?n1 ?b1 ?b2) and tuples (4 C A) and (5 B D), another table for the causal links involving the clear condition with schema (?n1 ?n2 ?b) and tuples (0 1 C), (0 2 B), (0 2 C), (0 3 B), (0 4 C), (0 5 B), (4 3 A) and (5 1 D), and similar tables for the other operator and link types. The match process consists of interpreting the rule antecedent as a conjunctive query with interpreted predicates, and executing this query against the relational view of the plan structures. As a running example, we will analyze the application of the avoid-move-twice rule of Figure 6 to the plan in Figure 4. Matching the rule antecedent identifies steps 1 and 4. More precisely, considering the antecedent as a query, the result is the single tuple (4 C A 1 D) for the variables (?n1 ?b1 ?b2 ?n2 ?b3).
After choosing a match to work on (line 3), the algorithm instantiates the subplan specified by the :replace field () according to such match (line 4) and removes the instantiated subplan from the original plan (line 5). All the edges incoming and emanating from nodes of the replaced subplan are also removed. The effects that the replaced plan was achieving for the remainder of the plan (), the UsefulEffects of , will now have to be achieved by the replacement subplan (or other steps of ). In order to facilitate this process, the AddFlaws procedure records these effects as open conditions.10 The result is the partial plan (line 5). Continuing with our example, Figure 14(a) shows the plan resulting from removing steps 1 and 4 from the plan in Figure 4.
Finally, the algorithm embeds the instantiated replacement subplan into the remainder of the original plan (lines 6-9). If the rule is completely specified, the algorithm simply adds the (already instantiated) replacement subplan to the plan, and no further work is necessary. If the rule is partially specified, the algorithm computes the embeddings of the replacement subplan into the remainder of the original plan in three stages. First, the algorithm adds the instantiated steps and links of the replacement plan (line 6) into the current partial plan (line 7). Figure 14(b) shows the state of our example after , the new stack step (6), has been incorporated into the plan. Note the open conditions (clear A) and on(C D). Second, the FindThreats procedure computes the possible threats, both operator threats and resource conflicts, occurring in the partial plan (line 7); for example, the threat situation on the clear(C) proposition between step 6 and 2 in Figure 14(b). These threats and the preconditions of the replacement plan are recorded by AddFlaws resulting in the partial plan . Finally, the algorithm completes the plan using rPOP, a partial-order causal-link planning procedure restricted to only reuse steps (i.e., no step addition) (line 8). rPOP allows us to support our expressive operator language and to have the flexibility for computing one or all embeddings. If only one rewriting is needed, rPOP stops at the first valid plan. Otherwise, it continues until exhausting all alternative ways of satisfying open preconditions and resolving conflicts, which produces all valid rewritings. In our running example, only one embedding is possible and the resulting plan is that of Figure 14(c), where the new stack step (6) produces (clear A) and on(C D), its preconditions are satisfied, and the ordering (6 2) ensures that the plan is valid.
The rewriting algorithm in Figure 13 is sound in the sense that it produces a valid plan if the input is a valid plan, or it outputs failure if the input plan cannot be rewritten using the given rule. Since this elementary plan-rewriting step is sound, the sequence of rewritings performed during PbR's optimization search is also sound.
Lemma 1 (Soundness of rPOP) Partial-order causal-link (POCL) planning without step addition () is sound.
Proof: In POCL planning, a precondition of a step of a plan is achieved either by inserting a new step or reusing a step already present in the current plan (the steps having an effect that unifies with the precondition). Forbidding step addition decreases the set of available steps that can be used to satisfy a precondition, but once a step is found rPOP proceeds as general POCL. Since, the POCL completion of a partial-plan is sound , is also sound.
Theorem 1 (Soundness of Plan Rewriting) RewritePlan (Figure 13) produces a valid plan if the input is a valid plan, or outputs failure if the input plan cannot be rewritten using the given rewriting rule .
Proof: Assume plan is a solution to a planning problem with goals and initial state . In POCL planning, a plan is valid iff the preconditions of all steps are supported by causal links (the goals are the preconditions of the goal step, and the initial state conditions are the effects of the initial step), and no operator threatens any causal link [53,65].
If rule does not match plan , the algorithm trivially returns failure (line 2). Assuming there is a match , after removing from the steps and links specified in (including all links - causal and ordering - incoming and outgoing from steps of ), the only open conditions that exist in the resulting plan are those that was achieving (line 5). Adding the instantiated replacement subplan introduces more open conditions in the partial plan: the preconditions of the steps of (line 7). There are no other sources of open conditions in the algorithm.
Since plan is valid initially, the only (operator and/or resource) threats present in plan (line 7) are those caused by the removal of subplan (line 3) and the addition of subplan (line 7). The threats may occur between any operators and causal links of regardless whether the operator or causal link was initially in or in . The threats in the combined plan can be effectively computed by finding the relative positions of its steps and comparing each causal link against the steps that may be ordered between the producer and the consumer of the condition in the causal link (FindThreats, line 7).
At this point, we have shown that we have a plan () with all the flaws (threats and open conditions) explicitly recorded (by AddFlaws in lines 5 and 7). Since is sound (Lemma 1), we conclude that will complete and output a valid plan , or output failure if the flaws in the plan cannot be repaired.
Corollary 1 (Soundness of PbR Search) The optimization search of PbR is sound.
Proof: By induction. Assume an initial valid plan and a single step rewriting search. By Theorem 1, the output is either a valid rewritten plan or failure. If the output is failure, the search is trivially sound. Assume there is a valid plan after rewriting steps. According to Theorem 1, applying a single rewriting rule to plan produces a valid plan or failure. Thus, an arbitrary number of rewritings produces a valid plan (or no plan), so PbR's search is sound.
Although RewritePlan is sound, it may certainly produce plans that do not have the minimal number of steps when faced with arbitrary rules. For example, imagine that the consequent of a rewriting rule specified two identical steps s1 and s2 (both having as only effects e1 and e2) and that the only flaws in were exactly the open conditions e1 and e2. Then, a sound but non step-minimal plan would be using s1 to satisfy e1 and using s2 to satisfy e2 (although each step by itself could satisfy both open conditions). PbR does not discard this plan because we do not make any restriction on the types of acceptable cost functions. If we had a cost function that took the robustness of the plan into account, a plan with both steps may be desirable.
We cannot guarantee that PbR's optimization search is complete in the sense that the optimal plan would be found. PbR uses local search and it is well known that, in general, local search cannot be complete. Even if PbR exhaustively explores the space of plan rewritings induced by a given initial plan and a set of rewriting rules, we still cannot prove that all solution plans will be reached. This is a property of the initial plan generator, the set of rewriting rules, and the semantics of the planning domain. The rewriting rules of PbR play a similar role as traditional declarative search control where the completeness of the search may be traded for efficiency. Perhaps using techniques for inferring invariants in a planning domain [35,34,68] or proving convergence of term and graph rewriting systems , conditions for completeness of a plan-rewriting search in a given planning domain could be obtained.
The design of a plan-rewriting algorithm depends on several parameters: the language of the operators, the language of the rewriting rules, the choice of full-specification or partial-specification rewriting rules, and the need for all rewritings or one rewriting as required by the search method.
The language of the operators affects the way in which the initial and rewritten plans are constructed. Our framework supports the expressive operator definition language described in Section 2.1. We provide support for this language by using standard techniques for causal link establishment and threat checking like those in Sage  and UCPOP .
The language of the antecedents of the rewriting rules affects the efficiency of matching. Our system implements the conjunctive query language that was described in Section 3.1.1. However, our system could easily accommodate a more expressive query language for the rule antecedent, such as a relationally complete language (i.e., conjunction, disjunction, and safe negation) , or a recursive language such as datalog with stratified negation, without significantly increasing the computational complexity of the approach in an important way, as we discuss in Section 3.1.4.
The choice of fully versus partially specified rewriting rules affects the way in which the replacement plan is embedded into the current plan. If the rule is completely specified, the embedding is already specified in the rule consequent, and the replacement subplan is simply added to the current plan. If the rule is partially specified, our algorithm can compute all the valid embeddings.
The choice of one versus all rewritings affects both the antecedent matching and the embedding of rule consequent. The rule matches can be computed either all at the same time, as in bottom-up evaluation of logic databases, or one-at-a-time as in Prolog, depending on whether the search strategy requires one or all rewritings. If the rule is fully-specified only one embedding per match is possible. But, if the rule is partially-specified multiple embeddings may result from a single match. If the search strategy only requires one rewriting, it must also provide a mechanism for choosing which rule is applied, which match is computed, and which embedding is generated (rPOP can stop at the first embedding or compute all embeddings). Our implemented rewriting algorithm has a modular design to support different combinations of these choices.