generated by UPMurphi are actually represented by a timed sequence of rules chosen by the planner to reach a goal state starting from the initial state. It is also possible to write support functions and procedures and call them in the condition, action, duration or weight expressions to further modularise the specification. 

Error conditions can be defined by means of the *invariant* **construct, which allows one to** 
describe the constraints that must be fulfilled by every system state and, as a consequence, the states that represent system errors. 

The system initial state is declared through the *startstate* **construct, which requires the user to** 
suitably initialise all the model state variables. Finally, to support planning problems, the CMurphi input language has been extended in UPMurphi to include the *goal* **construct, used to** define the properties that a planning goal state must satisfy. Moreover, UPMurphi provides two important features to ease the hybrid systems modelling activity: the type *real(m,n)* of real numbers (with m digits for the mantissa and n **digits for the** exponent), and the use of externally defined C/C++ functions in the modelling language. In this way, for example, one can use the C/C++ language constructs and library functions to model complex dynamics involving calculations on real values. Finally, UPMurphi can exploit several techniques that help to mitigate the well-known state explosion problem due to the memory requirements of explicit state space exploration algorithms. However, it is worth noting that memory-related problems are common to all the current planning algorithms, when the system dynamics involves real values and complex mathematical operations. In particular, the tool supports *bit compression* [28] and *hash compaction* **[29], [30] to reduce** 
the memory size of the system state representation, and a symmetry reduction algorithm to decrease the state space size by detecting equivalent states. 

Shortly, bit compression saves memory by using every bit of the *state descriptor***, the memory** 
structure maintaining the state variables, instead of aligning them on byte boundaries, whereas hash compaction stores compressed values (also called *state signatures***) instead of full state** 
descriptors. Together, these two techniques can dramatically reduce the memory needed to explore huge state spaces. 

## 4. Case Study: The Autonomous Planetary V**Ehicle**

This section presents a motivating case study where planning is applied to automatically control the engine of an autonomous vehicle during a planetary exploration mission. As described in the introduction, the rover model as well as the environmental conditions have been defined to be as general as possible, to achieve realistic results, and the generated plan will be optimised for the shortest time and the lowest energy consumption, as a real mission would require. 

## 4.1. **Rover Specifications**

The rover can be naturally modelled as a hybrid system, with several nonlinear characteristics. 

Thus, we have a dynamics very hard to compute, which makes planning quite difficult. The rover model used in our case study is based on the Mars exploration rover described in [31]. 

In general, an exploration rover moves on the planet surface to observe different phenomena and/or try some experiments. The rover can recharge its batteries through a solar panel, but recharge cannot take place continuously, and the energy from the panels is not enough to directly power the rover. Therefore, it must minimise the energy consumption in order to have always enough battery charge for the next activity.