Variable Elimination for Scalable Receding Horizon Temporal Logic Planning
(2015) American Control Conference, 2015 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:
https://lup.lub.lu.se/record/8167609
- author
- Fält, Mattias LU ; Raman, Vasumathi and Murray, Richard M.
- organization
- publishing date
- 2015
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- Discrete event systems, Predictive control for nonlinear systems, Autonomous systems
- host publication
- 2015 American Control Conference (ACC)
- pages
- 6 pages
- publisher
- IEEE - Institute of Electrical and Electronics Engineers Inc.
- conference name
- American Control Conference, 2015
- conference location
- Chicago, IL, United States
- conference dates
- 2015-07-01 - 2015-07-03
- external identifiers
-
- scopus:84940914767
- ISBN
- 9781479917730
- 978-1-4799-8684-2
- DOI
- 10.1109/ACC.2015.7171013
- language
- English
- LU publication?
- yes
- id
- 0f5a4504-c06b-4276-b1f3-7a9e5a740d85 (old id 8167609)
- date added to LUP
- 2016-04-04 13:41:01
- date last changed
- 2024-04-19 07:32:52
@inproceedings{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.}},
booktitle = {{2015 American Control Conference (ACC)}},
isbn = {{9781479917730}},
keywords = {{Discrete event systems; Predictive control for nonlinear systems; Autonomous systems}},
language = {{eng}},
pages = {{1917--1922}},
publisher = {{IEEE - Institute of Electrical and Electronics Engineers Inc.}},
title = {{Variable Elimination for Scalable Receding Horizon Temporal Logic Planning}},
url = {{https://lup.lub.lu.se/search/files/11330849/8167662.pdf}},
doi = {{10.1109/ACC.2015.7171013}},
year = {{2015}},
}