Formal Methods for Planning With Spatial Constraints

As autonomous robots move from enclosed environment to our everyday lives, we have to ask: How can we ensure that they work as expected and how can we even specify what it means to work as expected? Formal methods have proven to be useful in addressing these questions; temporal logics provide rich, rigorous, yet user-friendly specification formalism and formal synthesis offers a way to automatically generate a plan or a controller that provably satisfies the specification (or satisfies it to some guaranteed extent). 

 

In this talk, we will focus on specification of spatial constraints for motion planning in Signal Temporal Logic (STL). We will discuss quantitative semantics of STL to distinguish between more and less compliant motion plans, and present an RRT*-based motion planning algorithm that converges to the maximally satisfying plan. Then, we will look into shorter-horizon control problems with spatial constraints, such as unparking from a tight parking spot. We will discuss how to combine a construction of a library of feedback motion primitives and an over- and under-approximation of the collision space to either find a desired motion plan, prove path non-existence, or trigger refinement of the primitives and the collision space approximations.