Reachability within Hybrid Automata

The Reachability problem for Hybrid Automata is the problem of determining, given an automaton $H$, whether there is a trajectory of the timed transition system, $S^{t}_{H}$, that visits a state of the form $(v,{\bf x})$. In the context of Hybrid Automata, $v$ is typically an error state, so that Reachability questions are posed to determine whether an automaton is safe. In the context of planning, the Reachability question is equivalent to Plan Existence. As is discussed in Henzinger's paper henzinger, the general Reachability question for Hybrid Automata is undecidable. This is unsurprising, since introducing metric fluents with arbitrary behaviours into the language results in sufficient expressive power to model Turing Machine computations. Indeed, Helmert has shown helmert that even relatively simple operations on discrete metric variables are sufficient to create undecidable planning problems. However, under various constraints, Reachability is decidable for several kinds of hybrid system, including Initialised Rectangular Automata [Henzinger, Kopke, Puri, VaraiyaHenzinger et al.1998]. In the following discussion we restrict our attention to deterministic Initialised Rectangular Automata, focussing particularly on Timed Automata [Alur DillAlur Dill1994], Priced Timed Automata [Rasmussen, Larsen, SubramaniRasmussen et al.2004] and Initialised Singular Automata [HenzingerHenzinger1996] and their relationships with fragments of the PDDL family of languages.

To simplify the definition of Rectangular Automata we introduce the following definition:

Definition 27   Interval Constraint Any constraint on a variable $x$ of the form $x \bowtie c$ for a rational constant $c$ and $\bowtie \in \{\leq,<,=,>,\geq\}$ is an interval constraint. A conjunction of interval constraints is also an interval constraint.

Rectangular Automata are Hybrid Automata in which all initial, invariant and flow conditions are interval constraints, whose flow conditions refer only to variables in $\dot{X}$ and whose jump conditions are a conjunction of interval constraints and constraints of the form $x_i^\prime = x_i$. Rectangular Automata may be non-deterministic because the interval constraints that determine the initial, flow and jump conditions might not determine unique values for the variables they constrain. Initialised Rectangular Automata meet the additional constraint that for each control switch, $e$, from $v$ to $w$, if $flow(v)_i \neq flow(w)_i$ then $x_i^\prime = x_i$ does not appear in $jump(e)$.

Initialised Rectangular Automata are important because they represent the boundary of decidability for Hybrid Automata [Henzinger, Kopke, Puri, VaraiyaHenzinger et al.1998].

Since PDDL is a deterministic language, we are most interested in the deterministic version of Rectangular Automata. A Singular Automaton is a Rectangular Automaton with deterministic jumps and variables of finite slope (that is, the flow conditions determine a unique constant rate of change for each variable). It is initialised if each continuous variable is reset every time its rate of change is altered by the flow function. The fact that the variables have finite slope allows rates of change to be modified. Initialised Singular Automata allow the modelling of linear continuous change and the rate of change to be modified provided that the corresponding variable is reset when this occurs. This constraint prevents the modelling of stopwatches [Alur DillAlur Dill1994], so ensures decidability of the Reachability problem. Whilst quite expressive, such automata cannot capture the dynamics that arise in many continuous planning domains. For example, it would not be possible to model the effect, on the level of water in a tank, of adding a second water supply some time into the filling process. According to the reset constraint the level value would have to be reset to zero when the second water source is introduced.

A Timed Automaton is a Singular Automaton in which every variable is a clock (a one-slope variable). These automata can be used to model timed behaviour and to express constraints on the temporal separation of events [Alur DillAlur Dill1994]. However, they cannot be used to model the continuous change of other quantities because clocks cannot be used to store intermediate values. They can be stopped and reset to zero, but they cannot operate as memory cells. Alur and Dill dill prove that reachability is decidable in Timed Automata because the infinite part of the model (the behaviour of the clocks) can be decomposed into a finite number of regions. This demonstrates that the infinite character of Timed Automata can be characterised by an underlying finite behaviour. Helmert helmert used a similar regionalisation technique in proving that the plan existence question for planning models including certain combinations of metric conditions and effects remains decidable.

A Priced Timed Automaton is a Timed Automaton in which costs are associated with the edges and locations of the automaton. Costs are accumulated over traces and enable a preference ordering over traces. PTAs have been used to solve simple Linear Programming and scheduling problems [Rasmussen, Larsen, SubramaniRasmussen et al.2004]. Costs behave like clocks except that they can be stopped, or their rates changed, without being reset. To retain decidability despite the addition of cost variables their use is restricted: costs cannot be referred to in jump conditions although they can be updated following both edge and delay transitions. PTAs have been used to model planning problems in which actions are associated with linearly changing costs. For example, the Airplane scheduling bench mark, in which planes incur cost penalties for late and early landing, can be expressed in the syntax of PDDL+ and solved using PTA solution techniques [Rasmussen, Larsen, SubramaniRasmussen et al.2004]. The models are very restrictive: the dependence of the logical dynamics of the domain on the cost values cannot be expressed so costs cannot, for example, be used to keep track of resource levels during planning when resources are over-subscribed. However, they are capable of expressing a class of problems which require the modelling of continuous change and can therefore be seen as a fundamental step towards the modelling of mixed discrete-continuous domains.

Since PTAs allow the modelling of non-trivial planning domains with continuous change we begin by constructing a fragment of PDDL+ that yields state-space models exactly equivalent to PTAs. In the remainder of this section we then discuss the relationships between richer PDDL+ fragments and different automata.