Integrated Task and Motion Planning with Verification via Formal Methods

This proposal lays out a research plan to "lift" current state-of-the-art results combining discrete and continuous layers of planning in motion planning to the more difficult and more useful problem of task and motion planning. The impact of such research is quite broad, and the current advances in AI and motion planning have made research in this area a hot topic in the robotics community. The uniqueness of this plan lies largely in the proposal to develop tools for verification and falsification in parallel with the tools for task and motion planning. It is expected that doing so will lead to more practical tools for our current robot systems. The significance for NASA is quite broad. Generally, NASA wants to use robots for remote exploration and for collaboration with astronauts. NASA wants robots to perform tasks that are too dangerous (searching for damage on the exterior of the ISS), too remote (exploring Mars), or too difficult (moving heavy objects on the moon) for a human. By increasing the level of autonomy in robots and by ensuring that they function safely and correctly, the depth and extent of missions can be increased.