3.3 Summary condition relationships and algorithms

In order to derive summary conditions according to their definitions, we need to be able to recognize achieve, clobber, and undo relationships based on summary conditions as we did for basic CHiP conditions. We give definitions and algorithms for these, which build on constructs and algorithms for reasoning about temporal relationships, described in Appendix A.

Achieving and clobbering are very similar, so we define them together. Definition 11 states that plan $p_1$ must [achieve, clobber] summary precondition $c_2$ of $p_2$ if and only if for all executions of any two plans, $p_1'$ and $p_2'$, with the same summary information and ordering constraints as $p_1$ and $p_2$, the execution of $p_1'$ or one of its subexecutions would [achieve, clobber] an external precondition $\ell(c_2)$ of $p_2'$.

Definition 11   $$\begin{array}{@{}l@{}l@{}l} must&\_[achieve,clobber] \_preco... ...ndition(\ell(c_2),e_{p_2'}) \end{array} \end{array}\end{array}$$

Achieving and clobbering in- and postconditions are defined the same as Definition 11 but substituting ``in'' and ``post'' for ``pre'' and removing the last line for inconditions. Additionally substituting $\exists$ for $\forall$ gives the definitions of may achieve and clobber. Furthermore, the definitions of must/may-undo are obtained by substituting ``post'' for ``pre'' and ``undo'' for ``achieve'' in Definition 11. Note that, as mentioned in Section 2.5, achieving inconditions and postconditions does not make sense for this formalism.

Algorithms for these interactions are given in Figure 6 and Figure 7. These algorithms build on others (detailed in Appendix B) that use interval point algebra to determine whether a plan must or may assert a summary condition before, at, or during the time another plan requires a summary condition to hold. Similar to Definition 3 of must-achieve for CHiP conditions, Figure 6 says that $p'$ achieves summary condition $c$ if it must asserts the condition before it must hold, and there are no other plans that may assert the condition or its negative in between. The algorithm for may-achieve (in Figure 7) mainly differs in that $p'$ may assert the condition beforehand, and there is no plan that must assert in between. The undo algorithms are the same as those for achieve after swapping $c$ and $c'$ in all $must$/$may$-$assert$ lines.

Figure 6: Algorithm for whether a plan must achieve or clobber a summary condition

Figure 7: Algorithm for whether a plan may achieve or clobber a summary condition

The complexity of determining must/may-clobber for inconditions and postconditions is simply $O(c)$ to check $c$ conditions in $p'$. If the conditions are hashed, then the algorithm is constant time. For the rest of the algorithm cases, the complexity of walking through the summary conditions checking for $p''$ and $c''$ is $O(nc)$ for a maximum of $c$ summary conditions for each of $n$ plans represented in $P_{sum}$. In the worst case, all summary conditions summarize the same propositional variable, and all $O(nc)$ conditions must be visited.

Let's look at some examples of these relationships. In Figure 8a, $p' = equip\_M2\_tool$ may-clobber $c$ = $available$(M2)MaS in the summary preconditions of $p = produce\_G$ because there is some history where $equip\_M2\_tool$ ends before $produce\_G$ starts, and $calibrate\_M2$ starts after $produce\_G$ starts. In Figure 8b, $p' = build\_H$ must-achieve $c$ = $available$(H)MuF in the summary preconditions of $p = move\_H$. Here, $c'$ is $available$(H)MuL in the summary postconditions of $build\_H$. In all histories, $build\_H$ attempts to assert $c'$ before the $move\_H$ requires $c$ to be met, and there is no other plan execution that attempts to assert a condition on the availability of H. $equip\_M2\_tool$ does not may-clobber $c$ = $available$(M2)MuF in the summary preconditions of $build\_H$ even though $equip\_M2\_tool$ asserts $c'$ = $\neg available$(M2)MuL before $c$ is required to be met. This is because $calibrate\_M2$ must assert $\neg available$(M2)MuA between the time that $equip\_M2\_tool$ asserts $c'$ and when $c$ is required. Thus, $calibrate\_M2$ must-undo $equip\_M2\_tool$ 's summary postcondition. Because $calibrate\_M2$ cannot assert its postcondition $available$(M2)MuL before $build\_H$ requires $available$(M2)MuF, $calibrate\_M2$ must-clobber the summary precondition.

Figure 8: The production and facilities managers' plans partially expanded. a) The managers' plans unordered with respect to each other. b) $equip\_M2\_tool$ must clobber $available$(M2)MaL of $produce\_G$, and $calibrate\_M2$ must clobber $available$(M2)MuF of $build\_H$.