Certified Set Convergence for Piecewise Affine Systems via Neural Lyapunov Functions

TL;DR

This paper presents a novel framework for certifying set convergence in piecewise affine systems using neural Lyapunov functions, decoupling verification from policy learning to handle complex dynamics.

Contribution

It introduces a three-stage pipeline combining Hamilton-Jacobi reachability, Deep Sets controllers, and zonotope propagation for certified set convergence guarantees.

Findings

Certifies set convergence on benchmarks up to dimension six.

Handles systems with operator norms exceeding unity.

Achieves full strict set containment with constant-time online cost.

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.