Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verification of $L_1$ Adaptive Control using Verse Library: A Case Study of Quadrotors

Lin Song, Yangge Li, Sheng Cheng, Pan Zhao, Sayan Mitra, Naira Hovakimyan

TL;DR

Problem: verify $L_1$ adaptive control for an 18‑D quadrotor under parametric uncertainty and input delays. Approach: apply the Verse Library with DryVR-based reachability to certify transient performance and robustness of the geometric controller augmented with $L_1$ adaptation, including uncertain mass as an augmented state and delays. Findings: the approach yields verifiable robust transient performance and a nonzero delay margin, with tracking degrading gracefully as input delay increases. Significance: demonstrates the viability of formal verification for complex adaptive controllers in AAM and informs future work on learning-enabled components.

Abstract

$L_1$ adaptive control ($L_1$AC) is a control design technique that can handle a broad class of system uncertainties and provide transient performance guarantees. In this work-in-progress abstract, we discuss how existing formal verification tools can be applied to check the performance of $L_1$AC systems. We show that the theoretical transient performance and robustness guarantees of an $L_1$ adaptive controller for an 18-dimensional quadrotor system can be verified using the recently developed Verse reachability analysis tool. We will further consider the performance verification of $L_1$AC on systems with learning-enabled components.

Verification of $L_1$ Adaptive Control using Verse Library: A Case Study of Quadrotors

TL;DR

Problem: verify adaptive control for an 18‑D quadrotor under parametric uncertainty and input delays. Approach: apply the Verse Library with DryVR-based reachability to certify transient performance and robustness of the geometric controller augmented with adaptation, including uncertain mass as an augmented state and delays. Findings: the approach yields verifiable robust transient performance and a nonzero delay margin, with tracking degrading gracefully as input delay increases. Significance: demonstrates the viability of formal verification for complex adaptive controllers in AAM and informs future work on learning-enabled components.

Abstract

adaptive control (AC) is a control design technique that can handle a broad class of system uncertainties and provide transient performance guarantees. In this work-in-progress abstract, we discuss how existing formal verification tools can be applied to check the performance of AC systems. We show that the theoretical transient performance and robustness guarantees of an adaptive controller for an 18-dimensional quadrotor system can be verified using the recently developed Verse reachability analysis tool. We will further consider the performance verification of AC on systems with learning-enabled components.
Paper Structure (11 sections, 1 equation, 3 figures)

This paper contains 11 sections, 1 equation, 3 figures.

Table of Contents

  1. Introduction
  2. Problem Formulation
  3. Scenarios
  4. Plant --- Quadrotor Dynamics
  5. Controller --- Geometric Control with $\mathcal{L}_1$ Augmentation
  6. Uncertainty & Input Delays
  7. Verification Solution
  8. Solution of ordinary differential equation (ODE)
  9. Reachability Analysis
  10. Reachability analysis with Verse
  11. Experiments and Results

Figures (3)

  • Figure 1: Verification architecture of geometric tracking control with $\mathcal{L}_1$ augmentation using the Verse Library li2023verse.
  • Figure 2: Transient performance verification of $\mathcal{L}_1$AC subject to time-varying system parameters: performance of geometric control (left) and geometric control w/ $\mathcal{L}_1$AC (right)
  • Figure 3: Robust performance verification of $\mathcal{L}_1$AC in the presence of input delay and time-varying system parameters: with input delay of 60ms (left) and 120ms (right)