Appendix B: Algorithms for Must/May Asserting Summary Conditions

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 $P$ with a corresponding set of summary information $P_{sum}$, a set of ordering constraints $order$, and a set of histories $H$ including all histories where $E(h)$ only includes an execution $e$ of each plan in $P$ and $e$'s subexecutions, and $E(h)$ satisfies all constraints in $order$. 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.

Definition 14  

A summary condition $c$ summarizes a condition $\ell$ in condition set $conds$ of plan $p$ iff $c$ was added by the procedure for deriving summary information to a summary condition set of $p'$; $\ell=\ell(c)$; and either $c$ was added for $\ell$ in a condition set $conds$ of $p=p'$, or $c$ was added for a summary condition of a subplan of $p'$ that summarizes $\ell$ in $conds$ of $p$.

For example, $at$(bin1, A) is a precondition of the $start\_move$ plan for moving part A from bin1 to machine M1 (as given in Section 2.2). When deriving the summary conditions for $start\_move$, $at$(bin1, A) is added to the summary preconditions. Thus, the summary precondition $at$(bin1, A)MuF summarizes $at$(bin1, A) in the preconditions of $start\_move$.

Definition 15  

An execution $e$ of $p$ requires a summary condition $c$ to be met at $t$ iff $c$ is a summary condition in $p$'s summary information; there is a condition $\ell$ in a condition set $conds$ of $p'$ that is summarized by $c$; if $first(c)$, $t=t_s(e)$; if $last(c)$, $t=t_f(e)$; if $always(c)$, $t$ is within $(t_s(e), t_f(e))$; and if $sometimes(c)$, there is an execution of a subplan of $p$ in $d(e)$ that requires a summary condition $c'$ to be met at $t$, and $c'$ summarizes $\ell$ in $conds$ of $p'$.

So, basically, an execution requires a summary condition to be met whenever the conditions it summarizes are required. The execution of $build\_G$ has a summary precondition $at$(A,M1_tray1). This execution requires this summary condition to be met at $t_s$($build\_G$) because $at$(A, M1_tray1) is a precondition of $build\_G$'s first subplan that is summarized by $build\_G$'s summary precondition.

Definition 16  

An execution $e$ of $p$ attempts to assert a summary condition $c$ at $t$ iff $c$ is a summary condition in $p$'s summary information; there is a condition $\ell$ in a condition set $conds$ of $p'$ that is summarized by $c$; $\neg first(c)$; if $always(c)$, $t$ is in the smallest interval after $t_s(e)$ and before the start or end of any other execution that follows $t_s(e)$; if $last(c)$, $t=t_f(e)$; and if $sometimes(c)$, there is an execution of a subplan of $p$ in $d(e)$ that attempts to assert a summary condition $c'$ at $t$; and $c'$ summarizes $\ell$ in $conds$ of $p'$.

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 $build\_G$, $produce\_G\_on\_M1$, and $produce\_H$ all assert summary postconditions that M1 becomes available at $t_f$($build\_G$).

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 $c$ was required (asserted in $c$). Agents also need to detect when a summary postcondition would be asserted at the same time as another summary postcondition $c$ (asserted when $c$).

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 $equip\_M1$ attempted to assert the incondition that M1 was unavailable at the same time that $build\_G$ attempted to assert the postcondition that M1 was available, the incondition would be clobbered by the postcondition.

Table: Table for must-assert by/before algorithm

Table: Table for may-assert by/before algorithm

Table: Table for must/may-assert in algorithm

Table: Table for must/may-assert when algorithm

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 $existence$ of summary conditions in different decompositions. For the following definitions and algorithms of must- and may-assert, we assume $c$ and $c'$ are summary conditions of plans in $P$.

Definition 17  

$p'\in P$ must-assert $c'$ [by, before] $c$ iff for all histories $h\in H$ and all $t$ where $e$ is the top-level execution in $E(h)$ of some $p\in P$ that requires $c$ to be met at $t$, and $e'$ is the top-level execution of $p'$ in $E(h)$, there is a $t'$ where $e'$ attempts to assert $c'$ at $t'$, and [$t'\leq t$, $t'<t$].

The must-assert algorithm is described in Table 3. $p'$ must-assert $c'$ by $c$ iff $order$ 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 $order$ 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 $c'$ is a $sometimes$ ($\neg last$) postcondition of $p'$, and $c$ is an incondition of $p$ with any timing, $order$ must require that the end of $p'$ be before or at the start of $p$ in order for $p'$ to must-assert $c'$ by the time $c$ 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 $may$ relationships, the algorithm returns true iff none of the corresponding ordering constraints in the table are imposed by (can be deduced from) $order$.

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 $produce\_G$ plan. $produce\_G$ must-assert $c' = must$, $last$ $available$(G) before $c = must$, $first$ $available$(G) in the summary preconditions of $move\_G$ 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 $produce\_G$ attempts to assert $c'$ before the execution of $move\_G$ requires $c$ to be met. The algorithm verifies this by finding that the end of $produce\_G$ is ordered before the start of $move\_G$ (row 1 in Table 3). It is also the case that $equip\_M2\_tool$ may-assert $c' = must$, $last$ $\neg available$(M2) by $c = may$, $sometimes$ $available$(M2) in the summary preconditions of $produce\_G$ because the two plans are unordered with respect to each other, and in some history $equip\_M2\_tool$ can precede $produce\_G$. The algorithm finds that this is true since $equip\_M2$ is not constrained to start after the start of $produce\_G$ (row 2 in Table 4).

In Figure 8b, $move\_tool$ may-assert $c' = must$, $last$ $free$(transport1) in $c = may$, $sometimes$ $\neg free$(transport1) in $produce\_G$'s summary inconditions because in some history $move\_tool$ attempts to assert $c'$ during the time that $produce\_G$ is using transport1 to move part A to machine M2. In addition, $equip\_M2\_tool$ must-assert $c' = must$, $last$ $\neg available$(M2) when $c = may$, $last$ $available$(M2) in $produce\_G$'s summary postconditions because $equip\_M2\_tool$ attempts to assert $c'$ at the same time that $produce\_G$ requires $c$ to be met. The end of Section 3.3 gives other examples.