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.
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, . 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 . Update expressions are constructed using the ``primed'' form of the position-indexed variable for the lvalue2 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 , and 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 , and as Henzinger does, as the names of the position-indexed variables for the planning instance being interpreted and as an extra variable used to represent time-slip.
Derek Long 2006-10-09