In this project, we consider the problem of planetary exploration with a two-agent team composed of a Mars helicopter and Mars rover, tasked to collect a set of samples from the Mars surface. Due to the high cost and risk associated with such missions, it is critical to have strong correctness and performance guarantees on the robots’ behaviors. To aid this objective, we devise a mission specification framework and formally encode complex mission specifications used for real Mars exploration operations. We introduce Belief Space Temporal Logic (BeST) to capture temporal and uncertainty constraints, ranging from science campaign (e.g., getting samples from certain regions on Mars) to operational constraints such as maintaining certain accuracy over the vehicles’ state and the environment, inter-agent distance, energy level, etc.
The notional rover and copter are assumed to have stochastic motion and perception, and are tasked with collecting samples from a partially-known environment. The helicopter provides support in terms of exploring the environment on-demand. We propose a sampling-based control policy synthesis framework for the rover together with an online execution procedure, where exploration demands for the helicopter are generated. Exploration is necessary if insufficient knowledge is available to synthesize a control policy with sufficient success probability. In addition, a health monitor is attached to the execution procedure that triggers re-planning if a mismatch between the maintained environment map and the rover’s sensor observations is detected, e.g., if high-risk areas with sand or high slopes are encountered.
Ali-akbar Agha-mohammadi - Jet Propulsion Laboratory
President and Directors Fund