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.
Semantics of HAs
The semantic mapping between HAs and LTS
The following definitions are repeated from Henzinger's paper henzinger.
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.
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:
, such that
iff the closed proposition
is true, and
are both true. The set is called the state space of H.
- For each event
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
iff and there is a differentiable function
, with the first derivative
such that: (1)
and (2) for all reals
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.