Advanced

Variable Elimination for Scalable Receding Horizon Temporal Logic Planning

Fält, Mattias LU ; Raman, Vasumathi and Murray, Richard M. (2015) American Control Conference, 2015 In 2015 American Control Conference (ACC) p.1917-1922
Abstract
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... (More)
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. (Less)
Please use this url to cite or link to this publication:
author
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
keywords
Discrete event systems, Predictive control for nonlinear systems, Autonomous systems
in
2015 American Control Conference (ACC)
pages
6 pages
publisher
IEEE--Institute of Electrical and Electronics Engineers Inc.
conference name
American Control Conference, 2015
external identifiers
  • Scopus:84940914767
ISBN
9781479917730
DOI
10.1109/ACC.2015.7171013
language
English
LU publication?
yes
id
0f5a4504-c06b-4276-b1f3-7a9e5a740d85 (old id 8167609)
date added to LUP
2015-11-09 12:52:44
date last changed
2016-10-13 05:12:44
@misc{0f5a4504-c06b-4276-b1f3-7a9e5a740d85,
  abstract     = {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.},
  author       = {Fält, Mattias and Raman, Vasumathi and Murray, Richard M.},
  isbn         = {9781479917730},
  keyword      = {Discrete event systems,Predictive control for nonlinear systems,Autonomous systems},
  language     = {eng},
  pages        = {1917--1922},
  publisher    = {ARRAY(0x84d0760)},
  series       = { 2015 American Control Conference (ACC)},
  title        = {Variable Elimination for Scalable Receding Horizon Temporal Logic Planning},
  url          = {http://dx.doi.org/10.1109/ACC.2015.7171013},
  year         = {2015},
}