Title:Scalable Integrated Task and Motion Planning from Signal Temporal Logic Specifications

Abstract:This paper aims to develop formal methods to achieve a performance guaranteed integrated task and motion planning (ITMP) with respect to high-level specifications given by signal temporal logic (STL). It is a problem of practical importance because many safety-critical applications in robotics (e.g., navigation, manipulation, and surgery) and autonomous systems (e.g., unmanned aircraft and self-driving cars) require a correct-by-construction design for complex missions. Traditional approaches usually assumed a discretization of the continuous state space or a finite partition of the workspace. Instead, we propose an abstraction-free method that synthesis continuous trajectories with respect to given STL specifications directly. For this, our basic idea is to leverage incremental constraint solving by efficiently adding constraints on motion feasibility at the discrete level. Our approach solves the ITMP from STL specification problem using a scalable logic-based inference combined with optimization, which uses efficient solvers, i.e., satisfiability modulo theories (SMT) and linear programming (LP). Consequently, our method has potential to scale up to handle high dimensional continuous dynamics. The proposed design algorithms are proved to be sound and complete, and numerical results are given to illustrate the effectiveness of the design algorithms.