Models of Action Concurrency in Temporal Planning

1 Introduction

Temporal planning has traditionally been viewed as action sequencing + scheduling. This close connection between planning and scheduling has been visible in the use of constraintbased methods in solving hard large-scale scheduling and resource allocation problems, and during the last decade also in solving temporal planning problems, for example with the satisfiability problem of the propositional logic (SAT) [Rankooh and Ghassem-Sani, 2013] and its extensions such as Satisfiability modulo Theories (SMT) [Shin and Davis, 2005; Maris and R´egnier, 2008], or MILP [Dimopoulos and Gerevini, 2002]. Interestingly, in recent years researchers in temporal planning have been abandoning approaches that use one-off reductions to constraint or logic languages. A very recent exception to this is based on the NDL modeling language for which a discretization method for temporal planning was developed [Rintanen, 2015]. Most other recent works, using the standard PDDL modeling language [Fox and Long, 2003], split the temporal planning problem to first solving what is essentially a classical planning problem with all quantitative temporal information removed [Rankooh and Ghassem-Sani, 2013], followed by or interleaved with a separate scheduling phase to determine if all actions can be correctly scheduled. If the scheduling fails, the first phase is run again with additional constraints to rule out the same incorrect solution. No explanation has emerged why the more monolithic search methods that tightly integrate the action selection phase and the linear numeric constraint solving phase, such as MILP or SMT, have been mostly abandoned.

∗Also affiliated with Griffith University, Brisbane, Australia, and the Helsinki Institute for Information Technology, Finland. This work was funded by the Academy of Finland (Finnish Centre of Excellence in Computational Inference Research COIN, 251170).

In this work, we investigate mechanisms for constraining actions' concurrency and co-occurrence employed in temporal modeling languages used by the AI planning community, and argue that they explain why MILP or SMT have seemed unattractive. Specifically, we observe that PDDL 2.1 [Fox and Long, 2003] induces temporal gaps between consecutive interdependent actions, and these gaps often induce twice the number of steps in the plans than what is necessary, with strong negative performance implications. The gaps are caused by the management of implicit resources as manipulation of state variables, for which the PDDL 2.1 definition introduces what is essentially a 0-duration critical section that can be utilized by at most one of conflicting actions at a time.

Our results provide new support to the idea that modeling languages and problem modelings have far more impact on the practical usability of planning technologies than what is widely recognized, and that some of the current modeling languages for temporal planning are not well suited for many of the leading methods for solving realistic planning and scheduling problems, including constraint programming, mixed integer linear programming (MILP), and SAT-based methods including SAT modulo Theories (SMT).

The structure of the work is as follows. Section 2 discusses representations of action exclusion in PDDL and an alternative language. Section 3 discusses the computational implications of the two models. Section 4 outlines encodings in SMT. Section 5 analyzes mappings between the two modeling languages. Section 6 experiments with them. We conclude by listing topics for future research.

2 Models

We use two temporal modeling languages that respectively use the action exclusion mechanism from PDDL 2.1 [Fox and Long, 2003] and explicit resources as formalized in the NDL language [Rintanen, 2015], with extensions to support our results in Section 5.

We assume a familiarity of the propositional logic. If x is a state variable, then x and ¬x are literals. The complement l of literal l is defined by x = ¬x and ¬x = x. We define states as valuations v : X → {0, 1} of the state variables. Executions of temporal plans are infinite state sequences on the rational time line, represented by valuations v(t, x) of state variables for rational numbers t ≥ 0. As the definition of states coincides with the definition of models in the propositional logic, we denote by v(t, φ) the obvious generalization of the valuation to propositional formulas φ.

2.1 PDDL-Style Action Exclusions

An action consists of a precondition which determines whether an action can be taken at a given point of time, as far as the values of the state variables are concerned but ignoring other actions, and effects which determine how and when state variables change after the action has been taken.

Definition 1 (Actions) Let X be a finite set of state variables. An action is a pair 〈p, e〉 where

• the precondition p is a propositional formula over X,
• the effect e is a set of pairs (t, l) where t ≥ 0 is a rational number and l is a literal over X.

The precondition has to be true when the action is taken, and effects (t, l) cause literals l to be true a duration t after the action was taken. Define prec(〈p, e〉) = p and eff(〈p, e〉) = e.

We next give a formal definition of a simple modeling language that incorporates PDDL's action exclusion mechanism.

Definition 2 (Problem instance) A problem instance in temporal planning is a quadruple 〈X, I, A, G〉 where

• X is a set of state variables,
• I : X → {0, 1} is the initial state, describing the initial values of state variables,
• A is a set of actions over X, and
• G is the goal, a propositional formula over X.

Definition 3 (Plans and Executions) Given a problem instance 〈X, I,A,G〉, a plan π is a finite set of pairs (a, t), where t ≥ 0 is a rational number and a ∈ A is an action such that the following holds.

1. There is no {(a1, t1), (a2, t2)} ⊆ π such that
2. (a) x occurs in prec(a1), (b) (t, l) ∈ eff(a2) for l ∈ {x, ¬x}, and
3. (c) t1 = t2 + t.
4. There is an execution v : Q × X → {0, 1} which is a mapping from non-negative rational time points and state variables to 0 and 1 such that
5. (a) v(0, x) = I(x) for all x ∈ X,
6. (b) if (a, t) ∈ π, then for some ϵ > 0 and for all t′ such that t - ϵ < t′ < t we have v(t′ , prec(a)) = 1,
7. (c) if (a, t) ∈ π and (t′ , l) ∈ eff(a), then v(t + t′ , l) = 1,
8. (d) state variables not changed by actions retain their values: for any tl and tu such that tl < tu, if
9. v(tl, x) = 1, and
10. there is no (a, t′ ) ∈ π such that (t′′ , ¬x) ∈ eff(a) and tl ≤ t′ + t′′ ≤ tu

then v(ti, x) = 1 for all ti such that tl < ti ≤ tu. (Analogously for v(tl, x) = 0.)

1. There is t such that v(t′ ,G) = 1 for all t′ > t.

Condition 1 is the essence of action exclusions in PDDL: two actions cannot be taken simultaneously if the precondition of one is falsified by the start effect of the other.

Prevention of Actions' Overlap

In this modeling, the only mechanism for explicitly expressing constraints on the co-occurrence of actions is the ban on two actions starting at exactly the same time point according to Condition 1. Not being exactly simultaneous may seem insufficient for modeling non-overlapping, but this condition should only be viewed as a mechanism for creating a critical section in which state variables can be manipulated in ways that allow expressing more complex conditions on the overlap of actions. In particular, the critical sections allow the exclusive allocation of an implicit resource so that the overlap of actions is prevented: to make two actions exclusive, both actions have the same precondition x and the same effect (0, ¬x). Now the actions cannot be taken simultaneously, and since each action falsifies the precondition of the other, the second action cannot be taken before x is later made true.

Limits

The technically tricky part of the definition is the seeming simultaneity of the precondition x and the effect (0, ¬x). When an action is taken at some time point t0, the precondition x should be true at t0 and the effect (0, ¬x) should make x false at t0. Since a state variable cannot really be true and false simultaneously, we must interpret the truth of x in the precondition at t0 as the limit of truth of x as time approaches t0: x is "true" at t, as far as the precondition at t is concerned, if x is true at every time point t′ over some (possibly very short) interval ]t-ϵ, t[, where ϵ > 0. This is what our formalization of the truth of the precondition in (2b) of Definition 3 says. In terms of finite sets of actions taking place at different time points, this means that x becomes true at or before t - ϵ, and remains true until t.

2.2 Action Exclusions Based on Resources in NDL

Another model of exclusiveness of actions is resources [Le Pape, 1994], as used in NDL [Rintanen, 2015].

We formalize the resource-based action exclusion mechanism in NDL in order to compare it to the syntactic condition 1 in Definition 3. First we extend Definition 1 of actions by including an additional component, resource requirements.

Definition 4 (Actions with Resources) Let X be a finite set of state variables and R a finite set of resources. An action is a triple 〈p, q, e〉 where

• the precondition p is a propositional formula over X,
• the resource requirement q is a set of
• (ts , te , r) ⊆ Q×Q×R such that ts < te , and
• (ts , te , r, n) ⊆ Q×Q×R×N such that ts < te , and

• the effect e is a set of pairs (t, l) where t ≥ 0 is a rational number and l is a literal over X.

We consider two types of resource requirements, unary resources, expressed by the triples (ts , te , r), which model absolute exclusion inside a group of actions: at most one action at a time can allocate the resource r, as well as state resources, expressed by 4-tuples (ts , te , r, n), where n is the state. Multiple actions can use the same state resource as long as the required state n is the same. Hence state resources induce exclusions between sets of actions.

Definition of plans and executions (Definition 3) mostly remain unchanged for our second model. The action exclusion condition is changed. Additionally, preconditions are evaluated at the starting point of actions, not in the limit. Define prec(〈p, q, e〉) = p, eff(〈p, q, e〉) = e and rreq(〈p, q, e〉) = q.

Definition 5 (Plans and Executions with Resources)

Given a problem instance 〈X, R, I, A, G〉, a plan π is a finite set of pairs (a, t), where t ≥ 0 is a rational number and a ∈ A is an action such that

• (ts1 , te1 , r) ∈ rreq(a1) and (ts2 , te2 , r) ∈ rreq(a2), or
• (ts1 , te1 , r, n1) ∈ rreq(a1) and (ts2 , te2 , r, n2) ∈ rreq(a2) such that n1 ̸= n2

either

1. Exactly as in Definition 3, except for

We do not allow a precondition φ to be simultaneous with effects that make φ true.

Resource requirements (t0, t1, v) and (t0, t1, v, n) with t0 < t1 are interpreted as open intervals ]t0, t1[, and with t0 = t1 they are interpreted as closed intervals [t0, t0]. If we limited to durations > 0 only, it would suffice - from the point of view of allowing consecutive actions with a zero-duration gap between them - to have the intervals half-open. However, intervals [t0, t0] have important uses, and it sometimes is desirable to allow them between two open intervals.

3 Implications to Scheduling of Actions

Now we discuss the pragmatics of the temporal models formalized in Definitions 1, 2 and 3, and in Definitions 4 and 5. Our primary interest is in the implications of these models on constraint-based methods for temporal planning.

3.1 Timed PDDL

The core issue with PDDL 2.1 is that the start effect ¬x cannot possibly be simultaneous with the effect x of a preceding action, and hence there must be a gap of some non-zero duration between the actions.

Example 1 Consider the actions

which represent the movement of some (unnamed) object from location to location. Actions movea,b and movea,e are exclusive of each other because they both falsify the other's precondition as their first effect.

To move from a to d we need three actions. First movea,b is taken, starting at step 0 with effects at step 1. Then moveb,c follows, starting at step 2 with effects at step 3, and the final action is movec,d, starting at step 4 with effects at step 5. This is a total of 6 steps or explicitly represented states in the execution of the plan. These steps are for time points t0, . . . , t5, satisfying t1 = t0 + 2, t2 > t1, t3 = t2 + 2, t4 > t3, t5 = t4 + 2. The gaps (see Figure 1) between t1 and t2, and t3 and t4 can be arbitrarily small.

3.2 Explicit Resources and NDL

When using the NDL modeling language (Definitions 4 and 5), the at start effects that lead to the gaps shown in Figure 1 can be postponed to the end of the actions, and the evaluation of the preconditions at the start of the action - and not through the limit construction - allows action schedules without gaps.

Example 2 Consider the actions

Here x is a resource that could be intuitively associated with the object to be moved, allowing at most one move at a time.

With the NDL semantics, the action can be taken at the same time point where its precondition becomes true. Without the gaps the sequence of actions movea,b, moveb,c, movec,d only requires 4 steps (Figure 2): the starting points of each of the three actions (with the end point of the action coinciding with the starting point of the next) followed by the end point of the last action.

In general, when n consecutive actions each have a precondition that depends on the previous action, the PDDL modeling requires 2n steps, whereas with explicit resources n + 1 steps suffice. As is well known from Planning as SAT [Kautz and Selman, 1996], the number of steps is one of the most critical factors in the scalability of SAT solving. Halving the number of steps can improve performance exponentially.

4 Encodings of Timed Actions in SMT

Temporal planning can be reduced [Shin and Davis, 2005] to constraint-based formalisms such as SAT modulo Theories (SMT) [Wolfman and Weld, 1999].

In both SAT and SMT encodings the propositional variables encode the values of the state variables in a finite number of steps, numbered 0, . . . , T. Here T is the maximum number of consecutive actions (steps) in the plan. To represent temporal planning finitely, only those time points and states are represented in which (non-continuous) change takes place. This includes changes in discrete (Boolean) state variables [Shin and Davis, 2005]. Hence the explicit states are a sequence s0, . . . , sT for time points τ0 < τ1 < · · · < τT .

The SMT representation for the sequence s0, . . . , sT consists of state variables x encoded as propositional variables x@k for every k ∈ {0, . . . , T}, together with numeric variables ∆i = τi - τi-1, i ∈ {1, . . . , T} representing the differences of the absolute time points of consecutive steps.

4.1 PDDL-Style Encodings with Limits

We will be using a simplified variant of Shin and Davis' [2005] encoding of temporal PDDL planning in SMT. 1

In the following, we write φ@i for formulas φ with each state variable x replaced by x@i.

When an action is taken at step i, its precondition has to hold in the limit when approaching i. For discrete variables this limit equals the value of precondition in the preceding step. Hence preconditions p are encoded by

If action a has an effect l at time t (relative to the starting time of the action), then there must be a time point with a time difference t to the starting time.

If action a can make a literal l true at time t, then a contributes to the possible causes of l at step i by including

as one disjunct in the formula causesi(l) (with other disjuncts contributed by other actions.) Empty disjunctions are taken as constants false. The formula causesi(l) is used for expressing when a literal becomes true.

The formulas causesi(l) are also used in frame axioms to indicate the conditions under which the value of a state variable is the same in two consecutive steps.

The time that passes at each step has to be positive,

1 Since we do not use continuous variables, we can identify Shin and Davis' Q[T + i-1 ] with Q[T + i ].

and the ∆ and τ variables are related in the obvious way.

For every pair of actions a1 and a2 that should be exclusive because one falsifies the precondition of the other as its time 0 effect, we have

4.2 Limit-Free NDL Encodings with Resources

With the resource-based NDL language we can avoid the expression of the critical sections and limits that are needed for allocation of implicit resources in PDDL.

The encoding of the resource-based model is as above with the following modifications [Rintanen, 2015]. First, formula (8) is removed, as action exclusions are not based on the critical sections any more. Second, preconditions are evaluated in the starting step of an action instead of in the limit (represented by the preceding step). Hence we have

replacing (1). Third, we have additional formulas for representing resources, as described next.

Let actions a1 and a2 have conflicting resource needs respectively for intervals ]t0, t1[ and ]t2, t3[. If time t has passed since taking the first action, then for the second action to be possible at time 0, the following must hold.

If intervals overlap, the actions cannot be started at the same step, encoded as the obvious binary mutexes

When action a1 has been taken earlier, we use (10) to derive a constraint to prevent a2. The constraint is obtained as a disjunction that iterates over all past steps and tests whether the time t in (10) has passed since taking a1.

This formula says that if an action is taken, then its need for the resource starts after the need by another action ends, or its need ends before the need by another action starts. 2

5 Translating PDDL into NDL

We have developed a semi-automated translation process from PDDL into NDL. Theorem 1 illustrates many of the core issues, and allows partial translations for many of the standard benchmark problems, fully automated translation for Sokoban, and translations of most actions for Crewplanning and Elevators. Actions with PDDL's over all conditions require the use of state resources: the over all condition is replaced by the allocation of a state resource in state 1 for the action's duration, and any effect in other actions violating the condition is extended with the allocation of the same state resource in state 0 for a single time point.

2 Note that there may be O(n2 ) formulas (12) for n actions. In many important cases O(n) size encodings of resource constraints are possible, but these encodings are out of the scope of this work.

Theorem 1 has been expressed in terms of two NDL models that differ in some effects having been delayed from time point 0 to the last time point of the action. This is how PDDL's at start effects can be turned into at end effects if resource constraints can be used to make sure the change does not invalidate existing plans, provided that no new plans are enabled that incorrectly exploit the changed action definition.

We outline the process next. Let the action have an effect e at time 0. Let a1, . . . , an be all actions that depend on e, that is, their preconditions share a state variable with e. If all of a1, . . . , an are mutually exclusive (mutex) with a, then the effect e can be moved from 0 to the action's end time taend . By two actions being mutex we mean that resources or system properties [Rintanen, 2014] guarantee that the interval between the starting and ending points of the actions cannot overlap.

The exclusivity test is split into two parts. First, check that no action violates the exclusivity condition. Second, when the exclusivity condition otherwise holds, but would be violated by moving the effect, then the exclusivity has to be restored. We will discuss these next.

Consider an action a with effect ¬x at time 0. Hence x is (possibly) true until 0 and false after 0. Moving ¬x from 0 to taend could affect possible plans in three ways.

1. Actions depending on x could possibly be taken between 0 and taend where they otherwise could not be taken.
2. Actions depending on ¬x cannot be taken between 0 and taend where they otherwise could be taken.
3. Actions with effect x scheduled between the start and end of a could have their effect overridden if ¬x is moved from 0 to taend .

For the move to not produce new plans that are not valid according to the original problem description, taking actions of type 1 must be prevented. For the move to not invalidate existing plans, actions of types 2 and 3 must not exist.

The theorem presents a test for detecting actions of type 2 and 3 (preventing the move), and derives new constraints for forbidding actions of type 1 in the modified problem instance.

The theorem is given with ¬x as the effect to be moved, but it obviously holds when the roles of x and ¬x are reversed.

Theorem 1 Let P be a NDL problem instance with actions A. Let P ′ be an NDL problem instance obtained from P by delaying effects (0, l) to the end of the action by the following procedure. Let a be any action such that

1. ¬x is an effect of a at 0,
2. x is not an effect of a at any t′ > 0,
3. the last effects of a are at taend ,
4. a is mutex with every action that makes x true (and consequently, no other action can make x true between 0 and taend ),
5. a is mutex with every action with precondition ¬x (and consequently, no action depends on ¬x between 0 and taend ). 3

Action a is replaced by a modified action obtained by

1. moving effect ¬x from 0 to taend ,
2. adding resource requirement (0, taend ,Rx , 0),
3. adding resource requirement (0, 0,Rx , 1) to any action in A - {a} with x in the precondition, and
4. adding resource requirement (t, t,Rx , 1) to any action in A - {a} with effect (t, x).

Then any plan for P is also a plan for P ′ , and any plan for P ′ is also a plan for P.

Proof: Let π be any plan for P. Define P0 = P, and let P, . . . , Pn be NDL instances such that each Pi, i > 0 is obtained from Pi-1 by modifying one of the actions. Our proof shows that each Pi preserved the plans of Pi-1. We obtain P ′ as the last instance Pn in the sequence generated by modifying n actions.

Let π be any plan for Pi-1 with an occurrence of the action a that is modified. We show that π is also a plan for Pi.

• We show that same states will be generated. The difference between the two cases is that the effect ¬x of a is moved from 0 to taend . Until the starting point of a and starting from the end point of a the execution is the same in both cases. The changes possibly caused simultaneously by other actions are not affected by the postponement of ¬x. In particular, since no other action that could overlap with a can make x true (assumption 4), no effect of an overlapping action is overridden by the postponed ¬x.
• We show that all preconditions are satisfied. Again, the only change is postponing ¬x from 0 to taend in action a. Hence by assumption 5 there are no actions in π with a precondition that turns false when ¬x is delayed to taend .
• We show that the additional resource requirements in Pi are not violated. Since in π no action with x in the precondition starts (relative to the starting point of a) between 0 and taend (because x is false there), the additional resource requirements in Pi (which only concern this case) is satisfied.

For the proof in the other direction, assume that π is a plan for Pi. We show that π is also a plan for Pi-1.

• We show that same states will be generated. The difference between the two cases is that the effect ¬x of a is moved from taend to 0. Until 0 and starting from taend the execution is the same in both cases.

Resource requirement 4 guarantees that no action makes x true between 0 and taend . Hence the state at the end of action a with Pi-1 and Pi is the same.

• We show that all preconditions are satisfied. Again, the only change is move of ¬x from taend to 0 in action a. The

3 For many of the standard benchmarks a weaker condition suffices: ¬x is not in the precondition of any action in A- {a}.

Runtimes in seconds by instance

resource requirements 2 and 3 guarantee that no action with precondition x is taken between 0 and taend . Hence every precondition is satisfied for Pi-1 if every precondition is satisfied for Pi.

• Resource requirements for Pi-1 are not violated because the requirements for Pi-1 is a subset of those of Pi, and the latter are satisfied by assumption. □

Conditions of Theorem Theorem 1 explicitly rule out problems with required concurrency [Cushing et al., 2007]. Coles et al. [2009] show that compression-safe temporal actions can be replaced by classical ones. The conditions for compression-safety are distantly related to the conditions of Theorem 1, but our modeling language is different, our conditions more general, and our theorem is about mapping temporal actions to equivalent temporal actions, not to classical ones.

6 Experiments

We compare PDDL models to their NDL translations with problems from the 2008 and 2011 planning competitions. 4 We translated all PDDL models into NDL manually, although some of these translations, or parts of them, would have been possible to automate with Theorem 1.

We implemented fully automatic translations from PDDL 2.1 and NDL into SMT, and solved the benchmark problems with the Z3 SMT solver on a workstation cluster mostly consisting of mid-range Intel Xeon CPUs from about 2010 to 2012. The runtime per instance was limited to 30 minutes. For each instance, we generated SMT encodings for 3n steps, for all n > 0, and solved them one by one until a satisfiable SMT instance (corresponding to a plan) was encountered.

Figure 3 illustrates the performance improvements of NDL over PDDL, with a plot of runtimes with both models for instances solved in under 30 minutes. The typical performance gain is between one and three orders of magnitude. The numbers of instances solved in 30 minutes are given in Table 1. The weighted score is the sum of the fractions of instances solved for each domain.

4 Except for the rather complicated PARC Printer problem which we did not understand deeply enough to model it in NDL.

Rintanen [2015] reports further performance gains for NDL models obtained by discretizing the rational time line to integers. Interestingly, reformulating PDDL models into NDL improves performance roughly equally as the discretization of NDL models.

7 RelatedWork

Earlier research on temporal planning has not identified PDDL modeling to be a performance issue. This has probably been because of the general focus of the research area on explicit state-space search (forward-chaining) rather than constraint-based methods [Kautz and Selman, 1996] or other search methods including backward-chaining [Rintanen, 2008], and due to the research area taking existing problem modelings and modeling languages as given.

Approaches based on specialized algorithms for search with temporal states [Do and Kambhampati, 2003] and action schedules [Gerevini et al., 2010] do not suffer from the gaps the way all-encompassing reductions to SAT, SMT, MILP or CP with the leading encodings (as in Section 4) do. In these approaches, the requirement of having at least an ϵ gap preceding a precondition falsified by the same action's at start effects is merely an additional temporal constraint for action scheduling, with little or no performance implications. In contrast, in the state-of-the-art constraint based models of temporal planning, the gaps often double the number of steps in the planner, resulting in an exponential performance penalty, as demonstrated in Section 6.

Some recent constraint-based planners have avoided the issue with gaps by abstracting the temporal planning problem to a classical one, and performing action scheduling separately. The work on ITSAT is a prominent example of this category [Rankooh and Ghassem-Sani, 2013]. ITSAT, however, is incapable of effectively minimizing plan duration, as temporal information is ignored during search.

8 Conclusion

We have investigated the impact of problem modelings on the scalability of constraint-based planning methods. Our main finding is that problem modelings based on explicit manipulation of state variables for resource management lead to SMT encodings that are harder to solve than those based on an explicit notion of resources.

Promising directions for future research include partialorder methods which have earlier been very successful for classical planning [Rintanen et al., 2004; Wehrle and Rintanen, 2007; Robinson et al., 2009]. Planning-specific implementation technologies for SAT-solving [Rintanen, 2012] are obviously applicable also to SMT-based temporal planning.