Planning Autonomous Marine Inspection Tasks using SMT Encoding of Timelines

Abstract

A key challenge in autonomous vehicles is the high-level decision making required to be reactive to significant changes in the environment. Timeline-based planning is a paradigm for temporal (time-aware) task planning that can provide such high-level decisions. We present an algorithm for incrementally translating a timeline-based planning problem into satisfability modulo theories (SMT). Off-the-shelf SMT solvers have become very efficient, and using such a solver keeps our planner implementation relatively small, simple, and extensible. Compared to existing SMT translations, our approach typically produces smaller SMT problems, and our system shows promising performance on several benchmark problems. Our planning software was developed in the context of research projects on inspection operations for UUVs on subsea installations and for mobile robots on marine installations.