  Reach-avoid specifications are one of the most common tasks in autonomous
aerial vehicle (UAV) applications. Despite the intensive research and
development associated with control of aerial vehicles, generating feasible
trajectories though complex environments and tracking them with formal safety
guarantees remain challenging. In this paper, we propose a control framework
for a quadrotor UAV that enables accomplishing reach-avoid tasks with formal
safety guarantees. In this proposed framework, we integrate geometric control
theory for tracking and polynomial trajectory generation using Bezier curves,
where tracking errors are accounted for in the trajectory synthesis process. To
estimate the tracking errors, we revisit the stability analysis of the
closed-loop quadrotor system, when geometric control is implemented. We show
that the tracking error dynamics exhibit local exponential stability when
geometric control is implemented with any positive control gains, and we derive
tight uniform bounds of the tracking error. We also introduce sufficient
conditions to be imposed on the desired trajectory utilizing the derived
uniform bounds to ensure the well-definedness of the closed-loop system. For
the trajectory synthesis, we present an efficient algorithm that enables
constructing a safe tube by means of sampling-based planning and safe
hyper-rectangular set computations. Then, we compute the trajectory, given as a
piecewise continuous Bezier curve, through the safe tube, where a heuristic
efficient approach that utilizes iterative linear programming is employed. We
present extensive numerical simulations with a cluttered environment to
illustrate the effectiveness of the proposed framework in reach-avoid planning
scenarios.
