Merging Planning and Verication Techniques for \Safe Planning" in Space Robotics

Abstract

Space applications require software systems that are both autonomous and safe. Planning techniques can automatically generate plans that achieve given goals. Formal verication techniques, like model checking, can guarantee a higher degree of safety. In this paper, we combine planning and formal verication techniques in order to address the problem of \Safe Planning. By \Safe Planning, we mean the task of generating/validating plans that not only achieve the goal, but verify also a set of other user dened properties, e.g., safety properties. This work has been carried out in the context of \SACSO (SAfety Critical SOftware for planning in space robotics), a national project funded by the Italian Space Agency (ASI).