A Caltech Library Service

Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models

Fan, Chuchu and Miller, Kristina and Mitra, Sayan (2020) Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models. In: Computer Aided Verification. Lecture Notes in Computer Science. No.12224. Springer , Cham, pp. 629-652. ISBN 978-3-030-53287-1.

[img] PDF - Published Version
Creative Commons Attribution.


Use this Persistent URL to link to this item:


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.

Item Type:Book Section
Related URLs:
URLURL TypeDescription ReadCube access
Fan, Chuchu0000-0003-4671-233X
Miller, Kristina0000-0003-1016-1695
Mitra, Sayan0000-0001-7082-5516
Additional Information:© The Author(s) 2020. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. First Online: 14 July 2020. 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.
Funding AgencyGrant Number
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
Air Force Office of Scientific Research (AFOSR)FA8750-19-C-0089
Air Force Office of Scientific Research (AFOSR)FA9550-17-1-0236
Series Name:Lecture Notes in Computer Science
Issue or Number:12224
Record Number:CaltechAUTHORS:20211020-211306325
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:111559
Deposited By: Tony Diaz
Deposited On:22 Oct 2021 22:49
Last Modified:26 Oct 2021 19:35

Repository Staff Only: item control page