Verification of Design Specifications in L1 Adaptive Control

L-1 adaptive control (L(1)AC) theory gives uniform steady-state and transient performance bounds on state variables and control inputs and delay margin guarantees. These guarantees are strict and can be conservative as they are derived from the small gain theorem. On the other hand, a recently-developed verification tool - Verse [1] computes over-approximations of reachable sets from simulation data for particular problem instances and can provide more realistic and less conservative performance bounds. Prior work on the verification and validation (V&V) of control design specifications and performance metrics primarily centered on optimizing design parameters through optimization or parameter variable space exploration. However, analyzing highly nonlinear systems poses challenges in mathematical analysis and performance-bound quantification, leading to a case-by-case approach to observing the design guidelines. In this paper, we propose a general framework that leverages Verse to establish verification for L(1)AC design specifications. Furthermore, design guidelines for closed-loop nonlinear systems with L(1)AC are observed from the verification results and can be instructive for control development.