Proof of theorem

Given a PTA
we construct a PDDL+ model as follows. For each edge
, where is the clock constraint, is the action and is the subset of clock variables reset by this edge, we construct the following instantaneous action schema, called a *transition action*, which models the instantaneous transition from into .

(:action transition

:parameters ()

:precondition (and (in l) g)

:effect (and (assign () 0)

(increase (c) P(e))

(not (in l))

(in l)))

We also construct, for each location , the following process schema:

(:process process-location

:parameters ()

:precondition (in l)

:effect (and (increase (c) (* #t P(l))

(increase () (* #t 1))

))

Finally, we construct an event for each location:

(:event event-location

:parameters ()

:precondition (and (in l) (not (I(l))))

:effect (not (in l)))

The initial state specifies that each clock variable and the cost variable starts with value 0. It asserts `(in )`. The special error state is the empty state (if an event is triggered then it will remove the current location proposition, leaving it impossible to progress).

Note that this domain is valid PDDL+. No two actions can be applied in parallel because the system can only ever satisfy one condition of the form `(in )`.

For this construction to correctly capture the PTA, it remains to be shown that any PTA trajectory corresponds to a PDDL+ plan for this domain and that any plan corresponds to a trajectory.

Consider a (valid) PTA trajectory,

Similarly, given any valid PDDL plan for the above domain, the plan defines a trajectory by mapping the instantaneous actions into their corresponding edge transitions and the gaps between them into time delay transitions. The trajectory will be a valid one because of the construction of the actions and process models. Note that no valid plan can trigger an event, since this will leave the system in a state that cannot be progressed, preventing satisfaction of any goal. This means that invariant conditions for each location are always maintained.

We now consider the opposite direction of the proof: PDDL+ planning instances yield state space and transition models that can be expressed as PTAs with a constant factor transformation. We observe that the constraints on the PDDL+ language ensures that clock variables and a cost variable are distinguished and behave exactly as required for a PTA. In the ground state space, all states correspond directly to locations of a PTA and the legal actions that transition between states correspond to the edges of the corresponding PTA. With the exception of event transitions leading into an exceptional error state, each edge in a PDDL+ transition system will, by the constraints defining the language, always correspond to an instantaneous action and this action determines the clock constraints and reset effects of the corresponding PTA edge. Exactly one process is active in each state, and causes the variables to behave as clocks (except for the cost variable). The events govern the invariants for the states, causing any violation of an invariant condition to trigger a transition into an error state.

The correspondence between trajectories for the PTA defined in this way and plans for the PDDL+ transition system is immediate, subject to the same observations made above.