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 must [achieve, clobber] summary precondition of if and only if for all executions of any two plans, and , with the same summary information and ordering constraints as and , the execution of or one of its subexecutions would [achieve, clobber] an external precondition of .
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 for 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 achieves summary condition 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 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 and in all /- lines.
The complexity of determining must/may-clobber for inconditions and postconditions is simply to check conditions in . 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 and is for a maximum of summary conditions for each of plans represented in . In the worst case, all summary conditions summarize the same propositional variable, and all conditions must be visited.
Let's look at some examples of these relationships. In Figure 8a, may-clobber = (M2)MaS in the summary preconditions of because there is some history where ends before starts, and starts after starts. In Figure 8b, must-achieve = (H)MuF in the summary preconditions of . Here, is (H)MuL in the summary postconditions of . In all histories, attempts to assert before the requires to be met, and there is no other plan execution that attempts to assert a condition on the availability of H. does not may-clobber = (M2)MuF in the summary preconditions of even though asserts = (M2)MuL before is required to be met. This is because must assert (M2)MuA between the time that asserts and when is required. Thus, must-undo 's summary postcondition. Because cannot assert its postcondition (M2)MuL before requires (M2)MuF, must-clobber the summary precondition.