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

Fan, Chuchu; Miller, Kristina; Mitra, Sayan

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].

MSC:

93B50	Synthesis problems
93C10	Nonlinear systems in control theory

Software:

NumPy; PythonRobotics; TuLiP; FACTEST; pypoman; FaSTrack; SciPy; PESSOA; CoSyma; SCOTS; LTLMoP