The Relevance of HA Theory

Researchers concerned with the modelling of real-time systems have developed techniques for modelling and reasoning about mixed discrete-continuous systems [Yi, Larsen, PetterssonYi et al.1997,Henzinger, Ho, Wong-ToiHenzinger et al.1995,Rasmussen, Larsen, SubramaniRasmussen et al.2004]. These techniques have become well-established. The theory of hybrid automata [HenzingerHenzinger1996,Gupta, Henziner, JagadeesanGupta et al.1997,Henzinger RaskinHenzinger Raskin2000], which has been a focus of interest in the model-checking community for some years, provides an underlying theoretical basis for such work. As discussed in Section 2, the central motivation for the extensions introduced in PDDL+ is to enable the representation of mixed discrete-continuous domains. Therefore, the theory of hybrid automata provides an ideal formal basis for the development of a semantics for PDDL+.

Henzinger henzinger describes a digital controller of an analogue plant as a paradigmatic example of a mixed discrete-continuous system. The discrete states (control modes) and dynamics (control switches) of the controller are modelled by the vertices and edges of a graph. The continuous states and dynamics of the plant are modelled by vectors of real numbers and differential equations. The behaviour of the plant depends on the state of the controller, and vice versa: when the controller switches between modes it can update the variables that describe the continuous behaviour of the plant and hence bring about discrete changes to the state of the plant. A continuous change in the state of the plant can affect invariant conditions on the control mode of the controller and result in a control switch.

In a similar way, PDDL+ distinguishes processes, responsible for continuous change, from events and actions, responsible for discrete change. Further, the constraint in PDDL+, that numeric values only appear as the values of functions whose arguments are drawn from finite domains, corresponds to the requirement made in hybrid automata that the dimension of the automaton be finite.

An important contribution of our work is to demonstrate that PDDL+ can support succinct encodings of deterministic hybrid automata for use in planning. We expect that both the formal (semantics and formal properties) and practical (model-checking techniques) results in Hybrid Automata theory will be able to be exploited by the planning community in addressing the problem of planning for discrete-continuous planning domains. Indeed, some cross-fertilisation is already beginning [DierksDierks2005,Rasmussen, Larsen, SubramaniRasmussen et al.2004,EdelkampEdelkamp2003].