Algebraic verification for parameterized motion planning libraries

Recent progress in algorithms for estimating regions of attraction and invariant sets of nonlinear systems has led to the application of these techniques to motion planning in complex environments. In most instances, the verification occurs offline as the algorithms are still too computationally demanding for realtime implementation; as a result any online planner is restricted to applying the finite set of motion plans that were verified offline. In this paper we attempt to present a partial remedy by algebraically verifying families of parameterized feedback controllers. We provide a specific example using LQR controllers parameterized by their goal or nominal motion. We formulate this verification using robust region of attraction techniques in sums-of-squares optimization, and show that perturbations of a Lyapunov or Riccati equation can be used to provide algebraically parameterized Lyapunov candidates. The resulting verified “funnels” then provide a parameterized motion library that can be used efficiently in online planning. We present a number of numerical examples to demonstrate the effectiveness of our approach.