Fast and guaranteed safe controller synthesis for nonlinear vehicle models. (English) Zbl 1482.93185

Lahiri, Shuvendu Kumar (ed.) et al., Computer aided verification. 32nd international conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12224, 629-652 (2020).
Summary: 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.
For the entire collection see [Zbl 1453.68017].


93B50 Synthesis problems
93C10 Nonlinear systems in control theory
Full Text: DOI