Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reachability analysis for piecewise affine systems with neural network-based controllers

Dieter Teichrib, Moritz Schulze Darup

TL;DR

This work tackles the challenge of preserving stability and constraint satisfaction when neural networks approximate MPC laws for piecewise affine systems. It develops an MILP-based framework to compute over-approximations of k-step reachable sets, certify that the closed-loop system converges to a small positively invariant set containing the origin, and enforce state/output constraints without requiring a baseline controller. It further shows how to modify the NN controller to guarantee asymptotic stability via a dual-mode switching law and Lyapunov-based design, demonstrated on a four-region PWA example with a maxout NN. The approach integrates PWA dynamics, maxout NN activations, and MILP encodings to provide verifiable safety and stability guarantees for NN-controlled PWA systems, with potential extensions to faster conservatisms using alternative reachability methods.

Abstract

Neural networks (NN) have been successfully applied to approximate various types of complex control laws, resulting in low-complexity NN-based controllers that are fast to evaluate. However, when approximating control laws using NN, performance and stability guarantees of the original controller may not be preserved. Recently, it has been shown that it is possible to provide such guarantees for linear systems with NN-based controllers by analyzing the approximation error with respect to a stabilizing base-line controller or by computing reachable sets of the closed-loop system. The latter has the advantage of not requiring a base-line controller. In this paper, we show that similar ideas can be used to analyze the closed-loop behavior of piecewise affine (PWA) systems with an NN-based controller. Our approach builds on computing over-approximations of reachable sets using mixed-integer linear programming, which allows to certify that the closed-loop system converges to a small set containing the origin while satisfying input and state constraints. We also show how to modify a given NN-based controller to ensure asymptotic stability for the controlled PWA system.

Reachability analysis for piecewise affine systems with neural network-based controllers

TL;DR

This work tackles the challenge of preserving stability and constraint satisfaction when neural networks approximate MPC laws for piecewise affine systems. It develops an MILP-based framework to compute over-approximations of k-step reachable sets, certify that the closed-loop system converges to a small positively invariant set containing the origin, and enforce state/output constraints without requiring a baseline controller. It further shows how to modify the NN controller to guarantee asymptotic stability via a dual-mode switching law and Lyapunov-based design, demonstrated on a four-region PWA example with a maxout NN. The approach integrates PWA dynamics, maxout NN activations, and MILP encodings to provide verifiable safety and stability guarantees for NN-controlled PWA systems, with potential extensions to faster conservatisms using alternative reachability methods.

Abstract

Neural networks (NN) have been successfully applied to approximate various types of complex control laws, resulting in low-complexity NN-based controllers that are fast to evaluate. However, when approximating control laws using NN, performance and stability guarantees of the original controller may not be preserved. Recently, it has been shown that it is possible to provide such guarantees for linear systems with NN-based controllers by analyzing the approximation error with respect to a stabilizing base-line controller or by computing reachable sets of the closed-loop system. The latter has the advantage of not requiring a base-line controller. In this paper, we show that similar ideas can be used to analyze the closed-loop behavior of piecewise affine (PWA) systems with an NN-based controller. Our approach builds on computing over-approximations of reachable sets using mixed-integer linear programming, which allows to certify that the closed-loop system converges to a small set containing the origin while satisfying input and state constraints. We also show how to modify a given NN-based controller to ensure asymptotic stability for the controlled PWA system.

Paper Structure

This paper contains 11 sections, 9 theorems, 30 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Notation and definitions
  3. Fundamentals of MPC for PWA systems and neural networks with PWA activation
  4. Mixed-integer formulation of PWA system dynamics
  5. Mixed-integer formulation of NN with PWA activation
  6. Closed-loop analysis of PWA systems with neural network-based controller
  7. Reachability analysis
  8. Convergence to a set containing the origin
  9. Stability of the origin
  10. Case study
  11. Conclusions

Key Result

Lemma 1

Let $\boldsymbol{f}_{\text{PWA}}$ be as in eq:PWA_System and let $\boldsymbol{\Phi}(\boldsymbol{x})$ be a maxout NN as in eq:NN--eq:maxout. Then, any solution to the MI feasibility problem eq:MIClosedLoop is such that holds for all $k\in\{0,\dots,K-1\}$.

Figures (1)

  • Figure 1: Trajectories of the closed-loop system with the NN-based controller and the sets $\mathcal{X}$, $\mathcal{F}_{\text{max}}$, and $\mathcal{F}_{\text{min}}$, respectively. The initial states of the trajectories are specified in the legend and apply to all figures.

Theorems & Definitions (20)

  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Lemma 3
  • proof
  • Corollary 4
  • proof
  • Lemma 5
  • proof
  • ...and 10 more