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 conditionsummarizes 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 executionof
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 executionof
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.