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, $Q$, of states and a subset, $Q^{0} \subseteq Q$ of initial states.
• Transition Relation. A (possibly infinite) set, $A$, of labels. For each label $a \in A$ a binary relation $\stackrel {a}{\rightarrow}$ on the state space $Q$. Each triple $q \stackrel {a}{\rightarrow} q'$ is called a transition.

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:

• Define $Q,Q^{0} \subseteq V \times \mathbb{R}^{n}$, such that $(v,{\vec{x}}) \in Q$ iff the closed proposition $inv(v)[X:={\vec{x}}]$ is true, and $(v,{\vec{x}}) \in Q^{0}$ iff both $init(v)[X:={\vec{x}}]$ and $inv(v)[X:={\vec{x}}]$ are both true. The set $Q$ is called the state space of H.
• $A = \Sigma \cup \mathbb{R}_{\geq 0}$.
• For each event $\sigma \in \Sigma$, define $(v,{\vec{x}}) \stackrel {\sigma}{\rightarrow}(v',{\vec{x}'})$ iff there is a control switch $e \in E$ such that: (1) the source of $e$ is $v$ and the target of $e$ is $v'$, (2) the closed proposition $jump(e)[X,X':={\vec{x}},{\vec{x}'}]$ is true, and (3) $hevent(e) = \sigma$.
• For each non-negative real $\delta \in \mathbb{R}_{\geq 0}$, define $(v,{\vec{x}}) \stackrel {\delta}{\rightarrow}(v',{\vec{x}'})$ iff $v = v'$ and there is a differentiable function $f : [0,\delta]\rightarrow \mathbb{R}^{n}$, with the first derivative $\dot{f} : (0,\delta)\rightarrow \mathbb{R}^{n}$ such that: (1) $f(0) = {\vec{x}}$ and $f(\delta) = {\vec{x}'}$ and (2) for all reals $\epsilon \in (0,\delta)$, both $inv(v)[X:= f(\epsilon)]$ and $flow(v)[X,\dot{X}:= f(\epsilon),\dot{f}(\epsilon)]$ are both true. The function $f$ is called a witness for the transition $(v,{\vec{x}}) \stackrel {\delta}{\rightarrow}(v',{\vec{x}'})$.

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.