## 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.

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 non-negative 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 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