Semantics of HAs

Henzinger gives a semantics for HAs by constructing a mapping to Labelled Transition Systems [KellerKeller1976]. Figure 13 shows the complete semantic relationship between planning instances and labelled transition systems and between plans and accepting runs. The top half of the figure shows the relationship already constructed by Henzinger to give a semantics to Hybrid Automata. This completes the bridge between planning instances and labelled transition systems. The details of the mapping from Hybrid Automata to labelled transition semantics are provided in this section.

Figure 13: The semantic mapping between HAs and LTS

The following definitions are repeated from Henzinger's paper henzinger.

Definition 16   Labelled Transition System A labelled transition system, S, consists of the following components:

Definition 17   The Transition Semantics of Hybrid Automata The timed transition system $ S^{t}_{H}$ of the Hybrid Automaton $ H$ is the labelled transition system with components $ Q,Q^{0},A$ and $ \stackrel {a}{\rightarrow}$, for each $ a \in A$, defined as follows:

It is in this last definition that we see the requirement that each interval of continuous change in a timed transition system should be governed by a single set of differential equations, with a single solution as exhibited by the (continuous and differentiable) witness function.

The labelled transition system allows transitions that are arbitrary non-negative intervals of time, during which processes execute as dictated by the witness function for the corresponding period. In our definition of plans (Definition 3) we only allow rational times to be associated with actions, with the consequence that only rational intervals can elapse between actions. This means that plans are restricted to expressing only a subset of the transitions possible in the labelled transition system. We will return to discussion of this point in the following section, where we consider the relationship between plans and accepting runs explicitly.

Derek Long 2006-10-09