TY - GEN
T1 - Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models
AU - Fan, Chuchu
AU - Miller, Kristina
AU - Mitra, Sayan
N1 - Funding Information:
The authors acknowledge support from the DARPA Assured Autonomy under contract FA8750-19-C-0089, the Air Force Office of Scientific Research under grant AFOSR FA9550-17-1-0236, and the National Science Foundation under grant NSF CCF 1918531. The views, opinions and/or findings expressed are those of the authors and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.
Publisher Copyright:
© 2020, The Author(s).
PY - 2020
Y1 - 2020
N2 - We address the problem of synthesizing a controller for nonlinear systems with reach-avoid requirements. Our controller consists of a reference controller and a tracking controller which drives the actual trajectory to follow the reference trajectory. We identify a type of reference trajectory such that the tracking error between the actual trajectory of the closed-loop system and the reference trajectory can be bounded. Moreover, such a bound on the tracking error is independent of the reference trajectory. Using such bounds on the tracking error, we propose a method that can find a reference trajectory by solving a satisfiability problem over linear constraints. Our overall algorithm guarantees that the resulting controller can make sure every trajectory from the initial set of the system satisfies the given reach-avoid requirement. We also implement our technique in a tool FACTEST. We show that FACTEST can find controllers for four vehicle models (3–6 dimensional state space and 2–4 dimensional input space) across eight scenarios (with up to 22 obstacles), all with running time at the sub-second range.
AB - We address the problem of synthesizing a controller for nonlinear systems with reach-avoid requirements. Our controller consists of a reference controller and a tracking controller which drives the actual trajectory to follow the reference trajectory. We identify a type of reference trajectory such that the tracking error between the actual trajectory of the closed-loop system and the reference trajectory can be bounded. Moreover, such a bound on the tracking error is independent of the reference trajectory. Using such bounds on the tracking error, we propose a method that can find a reference trajectory by solving a satisfiability problem over linear constraints. Our overall algorithm guarantees that the resulting controller can make sure every trajectory from the initial set of the system satisfies the given reach-avoid requirement. We also implement our technique in a tool FACTEST. We show that FACTEST can find controllers for four vehicle models (3–6 dimensional state space and 2–4 dimensional input space) across eight scenarios (with up to 22 obstacles), all with running time at the sub-second range.
UR - http://www.scopus.com/inward/record.url?scp=85089234593&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85089234593&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-53288-8_31
DO - 10.1007/978-3-030-53288-8_31
M3 - Conference contribution
AN - SCOPUS:85089234593
SN - 9783030532871
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 629
EP - 652
BT - Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
A2 - Lahiri, Shuvendu K.
A2 - Wang, Chao
PB - Springer
T2 - 32nd International Conference on Computer Aided Verification, CAV 2020
Y2 - 21 July 2020 through 24 July 2020
ER -