Semantics of PDDL+

We present the semantics in two stages. In Section 6.2 we give the semantics of planning instances in terms of Hybrid Automata, by defining a formal mapping from planning constructs to constructs of the corresponding automata.

Figure 9: The semantic mapping between plans and traces

Figure 9 illustrates the syntactic relationship between a PDDL+ planning instance and the plans that it implies, and the semantic relationships both between the PDDL+ instance and the corresponding Hybrid Automaton and between the plans implied by the model and the traces implied by the automaton. The PDDL+ instance and its plans are syntactic constructs for which the HA and its traces provide a formal semantics. We show that, whilst plans can be interpreted as traces, traces can be represented as plans by means of the abstraction of events appearing in the traces. The figure represents the first stage in the development of our formalisation. We then summarise, in Section 6.3, Henzinger's interpretation of Hybrid Automata in terms of labelled transition systems and the accompanying transition semantics. We use this semantic step as the basis of the second stage of our formalism, as is shown in Figure 13.

The important distinction that we make in our planning models between actions and events requires us to introduce a time-slip monitoring process (explained below), which is used to ensure events are executed immediately when their preconditions are satisfied.

In Core Definition 4 we define how PNEs are mapped to a vector of position-indexed variables, $\vec{X} = \langle X_1,...,X_n \rangle$. The purpose of this mapping is to allow us to define and manipulate the entire collection of PNEs in a consistent way. The collection is given a valuation in a state as shown in Core Definition 2 where the logical and metric components of a state are identified. The updating function defined in Core Definition 8 specifies the relationship that must hold between the valuations of the PNEs before and after the application of an action. Normalisation of expressions that use PNEs involves replacing each of the PNEs with its corresponding position-indexed variable denoting its position in the valuation held within a state. This is performed by the semantic function $\mathcal{N}$. Update expressions are constructed using the ``primed'' form of the position-indexed variable for the lvalue² of an effect, to distinguish the pre- and post-condition values of each variable. In mapping planning instances to Hybrid Automata we make use of this collection of position-indexed variables to form the set of metric variables of the constructed automaton. In Definition 5, Henzinger uses the names $X$, $X^{\prime}$ and $\dot{X}$ for the vectors of variables, the post-condition variables following discrete updates and the derivatives of the variables during continuous change, respectively. In order to reduce the potential for confusion in the following, we note that we use $X$, $X^{\prime}$ and $\dot{X}$ as Henzinger does, $X_1, \ldots, X_{n}$ as the names of the position-indexed variables for the planning instance being interpreted and $X_{n+1}$ as an extra variable used to represent time-slip.