Hybrid Automata

We now present the relevant definition of a Hybrid Automaton from Henzinger's theory [HenzingerHenzinger1996] that will be used in the construction of our formal semantics for PDDL+ planning domains.

Definition 5   Hybrid Automaton A Hybrid Automaton H consists of the following components:

• Variables. A finite set $X = \{x_{1},\ldots ,x_{n}\}$ of real-valued variables. The number $n$ is called the dimension of H. We write $\dot{X}$ for the set $\{\dot{x}_{1}, \ldots ,\dot{x}_{n}\}$ of dotted variables, representing first derivatives during continuous change, and $X'$ for the set $\{x_{1}', \ldots ,x_{n}'\}$ of primed variables, representing values at the conclusion of discrete change.
• Control Graph. A finite directed graph $\langle V,E\rangle$. The vertices in V are control modes. The edges in E are control switches.
• Initial, invariant and flow conditions. Three vertex labelling functions, $init$, $inv$, and $flow$, that assign to each control mode $v \in V$ three predicates. Each initial condition $init(v)$ is a predicate whose free variables are from $X$. Each invariant condition $inv(v)$ is a predicate whose free variables are from $X$. Each flow condition $flow(v)$ is a predicate whose free variables are from $X \cup \dot{X}$.
• Jump conditions. An edge labelling function jump that assigns to each control switch $e \in E$ a predicate. Each jump condition $jump(e)$ is a predicate whose free variables are from $X \cup X'$.
• H-Events. A finite set $\Sigma$ of h-events and a function, $hevent : E \rightarrow \Sigma$, that assigns to each control switch an h-event.

An h-event is referred to by Henzinger as an $event$, but we have changed the name to avoid terminological confusion with events in PDDL+.

Figure 8 shows a very simple dynamic system expressed as a hybrid automaton.

Figure 8: A simple tank-filling situation modelled as a hybrid automaton. This has three control modes and three control switches. The control switch flood has a jump condition which requires the level to exceed the bath capacity. Flow conditions govern the change in water level.

The initial, jump and flow conditions are not necessarily satisfied by unique valuations. When multiple valuations satisfy these conditions it is possible for the behaviour of the automaton to be non-deterministic.

It should be observed that Henzinger's model needs to be extended, in a simple way, to include the undefined value, $\perp$, for real-valued variables. This is because PDDL+ states can contain unassigned real-valued variables, as shown in Core Definition 2 which defines the metric valuation of a state. The role of this value is to allow for the situations in which a metric fluent is created in a domain, but is not given an initial value. Such a fluent will be given the undefined value and attempts to inspect it before it is assigned a value will be considered to yield an error. This introduces no semantic difficulties and we have left the details of this modification implicit.

Just as the input language of a finite automaton can be defined to be the set of all sequences of symbols from its alphabet, it is possible to define the input language of a Hybrid Automaton. In this case, the elements of the language are called traces:

Definition 6   Trace Given a Hybrid Automaton, $H$, with h-event set $\Sigma$, a trace for $H$ is an element of the language $(\mathbb{R}_{\geq 0} \cup \Sigma)^{*}$.

Informally, a trace consists of a sequence of h-events interleaved with real values corresponding to time periods during which no h-events are applied. The time at which each h-event is applied is readily determined by summing the values of the time periods in the sequence up to the point at which the h-event appears: h-events take no time to execute. Note that this definition does not require that the trace is accepted by the Hybrid Automaton: this is a property of traces we consider in Section 6.4.

A further minor point to note is that the definition of a trace allows traces where the first transition occurs at time 0. Our convention in the semantics of PDDL2.1 is to forbid actions to occur at time 0. The reason for this is discussed in [Fox LongFox Long2003], but, briefly, in order to be consistent with the model in which states hold over an interval that is closed on the left and open on the right, the initial state (which holds at time 0) must persist for a non-zero interval. As a consequence, we will not be interested in traces that have action transitions at time 0.