activity, or at least to begin it, assuming that the vehicle is equipped with solar panels and in sunlight, so it can recharge its battery when needed. Moreover, the rover has to complete its task as soon as possible, since environmental conditions may quickly change, and in general a shorter task duration means that the rover will be able to perform more activities during the mission time. 

Unfortunately, also in this simplified setting, the rover still represents a hybrid system (i.e., described by both discrete and continuous variables), and the equations describing values such as energy consumption are usually nonlinear. Many efforts have been made to improve planning algorithms so as to cope with hybrid systems [4], however nonlinearity continues to be a relevant problem for many well-known planners such as TM-LPSAT [5], UPPAAL-TIGA [6] 
or MIPS [7]. Therefore, while a precise planning of the rover activities is important, automatically generating an optimal plan w.r.t. time and energy for the rover movements may be a hard task. 

## 1.1. **Contribution**

In this paper, which is an extended version of [8], we show how an explicit model checkingbased planner, namely UPMurphi [9], developed by the same authors, can be used to generate optimal plans to control a rover's engine, in order to move it for a specific distance in the least possible time, while satisfying a set of technical constraints and trying to save energy. 

Indeed, thanks to the model checking algorithms, UPMurphi is able to cope with systems showing high complexity and a behaviour that is difficult to predict, as hybrid nonlinear systems usually are. In the presented case study, the rover dynamics and behaviour, including some common technical constraints, have been modelled through general equations, that may apply to a wide range of vehicles. Plans have been optimised to minimise energy and time requirements, and the given minimal battery charge is always preserved. Therefore, the results are quite realistic. To the best of our knowledge, this is the first successful attempt to automatically generate time and resource-optimal plans for a rover model of such complexity. 

The paper is organised as follows. Section 2 shows some related work about planning algorithms and tools for hybrid and nonlinear systems. Section 3 describes the model checking approach to the planning problem and introduces the UPMurphi planner. Section 4 defines our case study and comments the planning results. Finally, Section 5 contains some closing remarks. 

## 2. Related Work

The planning problem presented in this paper can be generally defined as **planning with** 
resource consumption **[10], [11], [12].** 
Different techniques have been developed by the JPL [13] and applied to such kind of activity planning for NASA rovers. In particular, *the mixed initiative planning* **[14], supported by the** MAPGEN (Mixed-initiative Activity Plan GENerator) tool [15], [16] has been used for the Deep Space 1 mission. With this approach, humans and machines collaborate in the development and the management of plans: in particular, the user provides MAPGEN with a qualitative evaluation of the generated plan. 

The ASPEN [17], [18] framework has been used to perform activity planning for the Rocky 7 rover. In this framework, a first automatically generated plan is iteratively refined using different heuristics to finally fulfil the resource constraints. 

Finally, other approaches perform *planning with uncertainty***, mainly using probabilistic** 
methods [12], which however cannot handle problems with high complexity. 