Variable Elimination for Scalable Receding Horizon Temporal Logic Planning

Mattias Fält, Vasumathi Raman, Richard M. Murray
Submitted, 2015 American Control Conference (ACC)

Correct-by-construction synthesis of high-level re- active control relies on the use of formal methods to generate controllers with provable guarantees on their behavior. While this approach has been successfully applied to a wide range of systems and environments, it scales poorly with the increasing size of the environment. A receding horizon framework was recently proposed to mitigate this computational blowup, by decomposing the global control problem into several tractable subproblems. The existence of a global controller is ensured through symbolic checks of the specification, and local controllers are synthesized when needed, using the current state of the environment as the initial condition. This reduces the size of the synthesized strategy, but does not provide much improvement for problems with large dynamic environments, because the large number of possible global environment strategies. Ad hoc methods to locally restrict the environment have previously been used, at the risk of losing correctness. This paper presents a method of reducing specifications by eliminating locally redundant variables, while maintaining the correctness of controllers. We demonstrate the method using an autonomous car example, on problem sizes that were previously unsolvable due to the number of variables in the environment. We also demonstrate how the reduced specifications can be used to identify opportunities for reusing the synthesized local controllers.

• Conference Paper: http://www.cds.caltech.edu/~murray/preprints/frm15-acc s.pdf
• Project(s): SRC TerraSwarm