We address the problem of synthesizing a controller for nonlinear aerial vehicle models 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 or waypoints. We employ a machine learning-based framework to learn a tracking controller that can track any reference trajectory and simultaneously learn a tracking certificate 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 aerial vehicle satisfies the given reach-avoid requirement.
