Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Certified Set Convergence for Piecewise Affine Systems via Neural Lyapunov Functions

Yanliang Huang, Peng Xie, Zhen Zhang, Wenyuan Wu, Zhuoqi Zeng, Amr Alanwar

Abstract

Safety-critical control of piecewise affine (PWA) systems under bounded additive disturbances requires guarantees not for individual states but for entire state sets simultaneously: a single control action must steer every state in the set toward a target, even as sets crossing mode boundaries split and evolve under distinct affine dynamics. Certifying such set convergence via neural Lyapunov functions couples the Lipschitz constants of the value function and the policy, yet certified bounds for expressive networks exceed true values by orders of magnitude, creating a certification barrier. We resolve this through a three-stage pipeline that decouples verification from the policy. A value function from Hamilton-Jacobi backward reachability, trained via reinforcement learning, is the Lyapunov candidate. A permutation-invariant Deep Sets controller, distilled via regret minimization, produces a common action. Verification propagates zonotopes through the value network, yielding verified Lyapunov upper bounds over entire sets without bounding the policy Lipschitz constant. On four benchmarks up to dimension six, including systems with per-mode operator norms exceeding unity, the framework certifies set convergence with positive margin on every system. A spectrally constrained local certificate completes the terminal guarantee, and the set-actor is the only tested method to achieve full strict set containment, at constant-time online cost.

Certified Set Convergence for Piecewise Affine Systems via Neural Lyapunov Functions

Abstract

Safety-critical control of piecewise affine (PWA) systems under bounded additive disturbances requires guarantees not for individual states but for entire state sets simultaneously: a single control action must steer every state in the set toward a target, even as sets crossing mode boundaries split and evolve under distinct affine dynamics. Certifying such set convergence via neural Lyapunov functions couples the Lipschitz constants of the value function and the policy, yet certified bounds for expressive networks exceed true values by orders of magnitude, creating a certification barrier. We resolve this through a three-stage pipeline that decouples verification from the policy. A value function from Hamilton-Jacobi backward reachability, trained via reinforcement learning, is the Lyapunov candidate. A permutation-invariant Deep Sets controller, distilled via regret minimization, produces a common action. Verification propagates zonotopes through the value network, yielding verified Lyapunov upper bounds over entire sets without bounding the policy Lipschitz constant. On four benchmarks up to dimension six, including systems with per-mode operator norms exceeding unity, the framework certifies set convergence with positive margin on every system. A spectrally constrained local certificate completes the terminal guarantee, and the set-actor is the only tested method to achieve full strict set containment, at constant-time online cost.

Paper Structure

This paper contains 17 sections, 4 theorems, 22 equations, 3 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Problem Formulation
  3. PWA System Dynamics
  4. Zonotope Representation
  5. Control Objective
  6. Methodology
  7. Deep HJ as Lyapunov Guidance
  8. Set-Based Policy Distillation
  9. Theoretical Guarantees
  10. Numerical Experiments
  11. Benchmark Systems
  12. Training Configuration
  13. Results
  14. Pipeline Results
  15. Comparative Evaluation
  16. ...and 2 more sections

Key Result

Proposition 1

For a ReLU network with $D$ hidden layers and output-layer weights $W_{\mathrm{out}}$, satisfying $\|W_i\|_2 \leq \rho$ for all hidden layers, Lipschitz-based certification requires where $D_\Omega = \mathop{\mathrm{diam}}\nolimits(\Omega)$. For $\rho > 1$, this bound shrinks exponentially in $D$. For $\rho < 1$, $c_{\mathcal{T}}$ vanishes exponentially in $D$. $\blacktriangleleft$$\blacktriangle

Figures (3)

  • Figure 3: Certified set convergence for PWA systems over discrete time steps. An initial zonotope $Z_0$ evolves under action $a_0$ and, upon reaching mode boundaries at step $k{=}1$, splits into fragments that each evolve under distinct affine dynamics, distinguished by color. At every step, the set-actor produces a single control action $a_k$ that steers all fragments toward the target simultaneously. The fragments finally converge into the target $\mathcal{T}$, verified via zonotope propagation through the learned value function (Theorem \ref{['thm:traj_cert']}).
  • Figure 4: 8Sec benchmark, $M{=}8$ with non-axis-aligned boundaries. Left: Learned HJ value function $V^*(x)$ with eight mode boundaries shown dashed. The target $\mathcal{T}$ is located at the basin minimum, and contour lines show level sets. Right: Set-actor reachability from $Z_0 = \langle (-1,-1)^\top,\, 0.5I_2 \rangle$. Color encodes time step.
  • Figure 5: 4Quad reachability comparison. Left: Set-actor. Center: Oracle baseline. Right: $V^*$-Opt baseline. The oracle applies $\pi^*(c_k)$ without generator awareness, while $V^*$-Opt uses scenario-based fmincon optimization. Color encodes time step.

Theorems & Definitions (11)

  • Definition 1: Reachable Set Propagation
  • Proposition 1: Expressivity--Certifiability Barrier
  • proof
  • Theorem 1: Trajectory-Certified Set Convergence
  • proof
  • Remark 1: Over-Approximation and Hausdorff Inflation
  • Proposition 2: Diagnostic Sufficient Condition
  • proof
  • Theorem 2: Certified Terminal Convergence
  • proof
  • ...and 1 more