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:
 State Space. A (possibly infinite) set, , of states and a subset,
of initial states.
 Transition Relation. A (possibly infinite) set, , of labels. For each label a binary relation
on the state space . Each triple
is called a transition.
Definition 17
The Transition Semantics of Hybrid Automata
The timed transition system of the Hybrid Automaton is the labelled transition system with components and
, for each , defined as follows:
 Define
, such that
iff the closed proposition
is true, and
iff both
and
are both true. The set is called the state space of H.

.
 For each event
, define
iff there is a control switch such that: (1) the source of is and the target of is , (2) the closed proposition
is true, and (3)
.
 For each nonnegative real
, define
iff and there is a differentiable function
, with the first derivative
such that: (1)
and
and (2) for all reals
, both
and
are both true. The function is called a witness for the transition
.
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 nonnegative 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
20061009