@InProceedings{10.1007/978-3-030-53288-8_31, author="Fan, Chuchu and Miller, Kristina and Mitra, Sayan", editor="Lahiri, Shuvendu K. and Wang, Chao", title="Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models", booktitle="Computer Aided Verification", year="2020", publisher="Springer International Publishing", address="Cham", pages="629--652", abstract="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.", isbn="978-3-030-53288-8" }