A compositional algorithm for computing a switched system representation of neural network controllers

Abstract

Our broad motivation is to utilize the large body of work on verification techniques for switched affine systems towards verification of neural network-controlled systems. To this end, we explore the problem of computing a switched affine system (SAS) representation of neural network-controlled discrete-time linear dynamical systems by providing a compositional algorithm that computes the piecewise affine (PWA) representation of the neural network. Our algorithm relies on two subroutines - one that computes the PWA representation of a single layer of a neural network, and the other that computes the compositions of PWA representations. We introduce the concept of a composition ordering represented as a binary tree that specifies the order in which the layers of the neural network are composed, and use that to compute the PWA representation of the whole neural network. Our experimental evaluation highlights the critical parameters of the network affecting the runtime complexity. Finally, we illustrate the application of the PWA representation computation toward stability analysis of a neural network-controlled discrete-time linear dynamical system.