Here we describe algorithms for determining temporal plan relationships based on summary information. They are used to build other algorithms that determine whether plan must or may achieve, clobber, or undo the condition of another under particular ordering constraints.
The definitions and algorithms throughout this section are given within the context of a set of plans with a corresponding set of summary information , a set of ordering constraints , and a set of histories including all histories where only includes an execution of each plan in and 's subexecutions, and satisfies all constraints in . They are all concerned with the ordering of plan execution intervals and the timing of conditions. By themselves, they do not have anything to do with whether conditions may need to be met or must be met for a plan execution.
First, in order to determine whether abstract plan executions can achieve, clobber, or undo conditions of others, an agent needs to be able to reason about how summary conditions are asserted and required to be met. Ultimately, the agent needs to be able to determine whether a partial ordering of abstract plans can succeed, so it may be the case that an agent's action fails to assert a summary condition that is required by the action of another agent. Therefore, we formalize what it means for an action to attempt to assert a summary condition and to require that a summary condition be met. These definitions rely on linking the summary condition of a plan to the CHiP conditions it summarizes in the subplans of the plan's decompositions. Thus, we first define what it means for a summary condition to summarize these conditions.
A summary condition summarizes a condition in condition set of plan iff was added by the procedure for deriving summary information to a summary condition set of ; ; and either was added for in a condition set of , or was added for a summary condition of a subplan of that summarizes in of .
For example, (bin1, A) is a precondition of the plan for moving part A from bin1 to machine M1 (as given in Section 2.2). When deriving the summary conditions for , (bin1, A) is added to the summary preconditions. Thus, the summary precondition (bin1, A)MuF summarizes (bin1, A) in the preconditions of .
An execution of requires a summary condition to be met at iff is a summary condition in 's summary information; there is a condition in a condition set of that is summarized by ; if , ; if , ; if , is within ; and if , there is an execution of a subplan of in that requires a summary condition to be met at , and summarizes in of .
So, basically, an execution requires a summary condition to be met whenever the conditions it summarizes are required. The execution of has a summary precondition (A,M1_tray1). This execution requires this summary condition to be met at () because (A, M1_tray1) is a precondition of 's first subplan that is summarized by 's summary precondition.
An execution of attempts to assert a summary condition at iff is a summary condition in 's summary information; there is a condition in a condition set of that is summarized by ; ; if , is in the smallest interval after and before the start or end of any other execution that follows ; if , ; and if , there is an execution of a subplan of in that attempts to assert a summary condition at ; and summarizes in of .
We say that an execution ``attempts'' to assert a summary condition because asserting a condition can fail due to a simultaneous assertion of the negation of the condition. Like the example above for requiring a summary condition, the executions of , , and all assert summary postconditions that M1 becomes available at ().
In order for agents to determine potential interactions among their abstract plans (such as clobbering or achieving), they need to reason about when a summary condition is asserted by one plan in relation to when it is asserted or required by another. Based on interval or point algebra constraints over a set of abstract plans, an agent specifically would need to be able to determine whether a plan would assert a summary condition before or by the time another plan requires or asserts a summary condition on the same state variable. In addition, to reason about clobbering inconditions, an agent would need to determine if a summary condition would be asserted during the time a summary incondition was required (asserted in ). Agents also need to detect when a summary postcondition would be asserted at the same time as another summary postcondition (asserted when ).
We do not consider cases where executions attempt to assert a summary in- or postcondition at the same time an incondition is asserted because in these cases, clobber relations are already detected because executions always require the summary inconditions that they attempt to assert. For example, if attempted to assert the incondition that M1 was unavailable at the same time that attempted to assert the postcondition that M1 was available, the incondition would be clobbered by the postcondition.
In the case that the ordering constraints allow for alternative synchronizations of the abstract plans, the assertions of summary conditions may come in different orders. Therefore, we formalize must-assert and may-assert to determine when these relationships must or may occur respectively. As mentioned at the beginning of Section 9, this use of ``must'' and ``may'' is based only on disjunctive orderings and not on the of summary conditions in different decompositions. For the following definitions and algorithms of must- and may-assert, we assume and are summary conditions of plans in .
must-assert [by, before] iff for all histories and all where is the top-level execution in of some that requires to be met at , and is the top-level execution of in , there is a where attempts to assert at , and [, ].
The must-assert algorithm is described in Table 3. must-assert by iff entails the relationship given for the row corresponding to the type and timing of the two conditions. Rows of the table indicate the timing of both summary conditions and the constraints that must dictate for must-assert to be true. 'T' and 'F' in the table indicate whether the timing in the column is true or false for the condition. '?' means that timing doesn't matter for that condition in this case. For example, row 9 says that for the case where is a () postcondition of , and is an incondition of with any timing, must require that the end of be before or at the start of in order for to must-assert by the time is asserted or required.
The definitions and algorithms for the other assert relationships are similar. Tables 4-6 describe the logic for the other algorithms. For relationships, the algorithm returns true iff none of the corresponding ordering constraints in the table are imposed by (can be deduced from) .
We illustrate these relationships for the example in Figure 8. In Figure 8a the agents' plans are unordered with respect to each other. Part G is produced either on machine M1 or M2 depending on potential decompositions of the plan. must-assert , (G) before , (G) in the summary preconditions of because no matter how the plans are decomposed (for all executions and all histories of the plans under the ordering constraints in the figure), the execution of attempts to assert before the execution of requires to be met. The algorithm verifies this by finding that the end of is ordered before the start of (row 1 in Table 3). It is also the case that may-assert , (M2) by , (M2) in the summary preconditions of because the two plans are unordered with respect to each other, and in some history can precede . The algorithm finds that this is true since is not constrained to start after the start of (row 2 in Table 4).
In Figure 8b, may-assert , (transport1) in , (transport1) in 's summary inconditions because in some history attempts to assert during the time that is using transport1 to move part A to machine M2. In addition, must-assert , (M2) when , (M2) in 's summary postconditions because attempts to assert at the same time that requires to be met. The end of Section 3.3 gives other examples.