A Caltech Library Service

Variable elimination for scalable receding horizon temporal logic planning

Fält, Mattias and Raman, Vasumathi and Murray, Richard M. (2015) Variable elimination for scalable receding horizon temporal logic planning. In: 2015 American Control Conference (ACC). IEEE , Piscataway, NJ, pp. 1917-1922. ISBN 978-1-4799-8685-9.

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item:


Correct-by-construction synthesis of high-level reactive 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. A receding horizon framework mitigates 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. This reduces the size of the synthesized strategy, but still scales poorly for problems with dynamic environments because of the large number of environment strategies in each subproblem. Ad-hoc methods to locally restrict the environment come with the risk of losing correctness. We present a method for reducing the size of these subproblems by eliminating locally redundant variables, while maintaining correctness of the local (and thus global) 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.

Item Type:Book Section
Related URLs:
URLURL TypeDescription DOIArticle
Murray, Richard M.0000-0002-5785-7481
Additional Information:© 2015 AACC. This work was supported in part by TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA.
Funding AgencyGrant Number
Microelectronics Advanced Research Corporation (MARCO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
Semiconductor Research CorporationUNSPECIFIED
Record Number:CaltechAUTHORS:20160318-094020866
Persistent URL:
Official Citation:M. Fält, V. Raman and R. M. Murray, "Variable elimination for scalable receding horizon temporal logic planning," American Control Conference (ACC), 2015, Chicago, IL, 2015, pp. 1917-1922. doi: 10.1109/ACC.2015.7171013
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:65476
Deposited By: Tony Diaz
Deposited On:18 Mar 2016 16:46
Last Modified:03 Oct 2019 09:47

Repository Staff Only: item control page