Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reach-Avoid Control Synthesis for a Quadrotor UAV with Formal Safety Guarantees

Mohamed Serry, Haocheng Chang, Jun Liu

TL;DR

This work addresses formal-safety reach-avoid control for a quadrotor by integrating geometric tracking control with Bézier-trajectory synthesis. It accounts for tracking errors during planning by deriving uniform bounds and proving local exponential stability of the error dynamics for any positive gains, enabling safe trajectory synthesis within a guaranteed safe tube. A planning pipeline combines inflation/deflation of domains with safe hyper-rectangular sets and an RRT to generate a tube, followed by a heuristic iterative linear-programming procedure to produce a piecewise Bézier trajectory that remains inside the tube and respects state and control limits. Numerical simulations in cluttered environments demonstrate successful reach-avoid behavior, obstacle avoidance, and adherence to velocity and thrust bounds, validating the practical viability of the approach.

Abstract

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.

Reach-Avoid Control Synthesis for a Quadrotor UAV with Formal Safety Guarantees

TL;DR

This work addresses formal-safety reach-avoid control for a quadrotor by integrating geometric tracking control with Bézier-trajectory synthesis. It accounts for tracking errors during planning by deriving uniform bounds and proving local exponential stability of the error dynamics for any positive gains, enabling safe trajectory synthesis within a guaranteed safe tube. A planning pipeline combines inflation/deflation of domains with safe hyper-rectangular sets and an RRT to generate a tube, followed by a heuristic iterative linear-programming procedure to produce a piecewise Bézier trajectory that remains inside the tube and respects state and control limits. Numerical simulations in cluttered environments demonstrate successful reach-avoid behavior, obstacle avoidance, and adherence to velocity and thrust bounds, validating the practical viability of the approach.

Abstract

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.
Paper Structure (23 sections, 22 theorems, 108 equations, 8 figures, 2 algorithms)

This paper contains 23 sections, 22 theorems, 108 equations, 8 figures, 2 algorithms.

Table of Contents

  1. INTRODUCTION
  2. Preliminaries
  3. Positive definite matrices
  4. Special orthogonal and skew-symmetric matrices
  5. Differential inequalities
  6. Bézier curves
  7. Quadrotor Model
  8. Problem Formulation
  9. Geometric Control and Error Dynamics
  10. Stability Analysis
  11. Local exponential stability
  12. Uniform bounds
  13. Well-definedness of the closed-loop quadrotor system over any arbitrary time interval.
  14. Trajectory Generation
  15. Computing a safe tube
  16. ...and 8 more sections

Key Result

Lemma 1

Given $M,W\in \mathcal{S}^{n}_{++}$ and $x,\in \mathbb{R}^{n}$, and $A\in \mathbb{R}^{m\times n}$, we have

Figures (8)

  • Figure 1: The environment with ten obstacles as red boxes, one target set as the blue box, and the starting point as the blue asterisk. The top left corner is the view along the negative direction of the y-axis, and the top right corner is the view along the positive direction of the x-axis.
  • Figure 2: The safe tube is the union of the cyan boxes. Note that the safe tube does not intersect with the unsafe set (union of the light red boxes), where the last box of the safe tube lies within the target set (blue box).
  • Figure 3: The generated desired trajectory $p_{d}$ is shown as the blue curve, which lies within the safe tube (union of cyan boxes).
  • Figure 4: Sample points approximating the safe initial set characterized by \ref{['eq:InitialSet']} (the red points satisfy \ref{['eq:InitialSet']}, whereas the blue points do not satisfy \ref{['eq:InitialSet']}). The top left panel shows a 3D scatter plot of the sample points with position error assuming $e_v(0) = e_R(0) = e_\omega(0) = 0_{3}$, while the top right panel displays a cross-sectional view when ${e_p}_2(0) = 0$. The bottom left panel shows a 3D scatter plot of the sample points with attitude error assuming $e_p(0) = e_v(0) = e_\omega(0) = 0_{3}$, while the bottom right panel displays a cross-sectional view when ${e_R}_2(0) = 0$.
  • Figure 5: The generated twenty position trajectories going through the operating domain, avoiding the unsafe set (red boxes) and reaching the target set (blue box). The top right subplot is a zoomed-in view of the trajectories at the initial portion of the simulations.
  • ...and 3 more figures

Theorems & Definitions (28)

  • Lemma 1: See the proof in the Appendix
  • Lemma 2
  • Lemma 3
  • Lemma 4
  • Lemma 5
  • Lemma 6: See the proof in the Appendix
  • Remark 1
  • Remark 2
  • Proposition 1: See the proof in the Appendix
  • Lemma 7
  • ...and 18 more