Author ORCID Identifier

https://orcid.org/0000-0002-7724-8878

Date Available

9-26-2025

Year of Publication

2025

Document Type

Doctoral Dissertation

Degree Name

Doctor of Philosophy (PhD)

College

Engineering

Department/School/Program

Mechanical Engineering

Faculty

Hasan Poonawala

Abstract

This thesis develops a framework for analyzing the stability and invariance properties of closed-loop dynamical systems whose dynamics are derived from neural networks with rectified linear units (ReLUs). The ReLU neural network defines continuous piecewise affine (PWA) functions, which makes them ideal for analysis using polyhedral geometry and optimization techniques. To begin, we introduce two exact algorithms for enumerating polytopic regions of affine behavior induced by ReLU networks: a half-space-based method that checks the feasibility of activation patterns and a geometric vertex-based method. Using these methods, we are able to perform precise region-wise analysis, and these methods serve as the foundation for the rest of the thesis. Following this, we present an automated method for verifying Lyapunov stability in systems with closed-loop dynamics derived from ReLU networks. By converting Lyapunov conditions into quantifier-free linear constraints over each region of the domain, we enable efficient verification and synthesis of Lyapunov functions based on ReLU neural networks. We propose two refinement strategies to enhance the expressiveness of the candidate Lyapunov function: one based on the sign variation of the Lyapunov derivative, and the other based on directional variations in the vector field across region boundaries. To analyze invariance, we develop a barrier-function-based framework aligned with the PWA structure of ReLU-modeled systems. We introduce the use of a leaky ReLU function as the K-infinity function in the barrier condition to improve flexibility while retaining tractability. This facilitates the synthesis of valid barrier certificates by enabling compatibility with non-smooth formulations. To expand the certified invariant set, we propose the Union of Invariant Sets (UIS) method, in which multiple ReLU-based barrier functions are merged into a single certificate. To reduce conservatism from full-domain analysis, we introduced SEROAISE (Sequential Estimation of Region of Attraction via Invariant Set Estimation), a framework that first certifies an invariant set using a barrier function and then limits Lyapunov verification to that region. Our method of expanding the certified invariant set is Non-Uniform Growth of Invariant Sets (NUGIS), which selectively includes boundary points that satisfy the invariance condition. Lastly, the framework integrates a control policy refinement step that modifies ReLU-based closed-loop dynamics to obtain a larger invariant set. Together, these contributions provide a unified, automation-friendly methodology for certifying stability and forward invariance in systems with closed-loop dynamics derived from ReLU. The framework is validated through numerical experiments across a range of nonlinear control scenarios.

Digital Object Identifier (DOI)

https://doi.org/10.13023/etd.2025.461

Download

Share

COinS