Learning Koopman-based Stability Certificates for Unknown Nonlinear Systems

TL;DR

This paper introduces a novel framework that combines Koopman operator theory, neural networks, and formal verification to learn stability certificates for unknown nonlinear systems from limited, low-frequency data.

Contribution

It develops a method to simultaneously learn system dynamics and Lyapunov functions with formal stability guarantees using low-sampling data.

Findings

Learned Lyapunov functions can be verified with SMT solvers.

Provides less conservative estimates of the region of attraction.

Effective with limited and low-frequency data.

Abstract

Koopman operator theory has gained significant attention in recent years for identifying discrete-time nonlinear systems by embedding them into an infinite-dimensional linear vector space. However, providing stability guarantees while learning the continuous-time dynamics, especially under conditions of relatively low observation frequency, remains a challenge within the existing Koopman-based learning frameworks. To address this challenge, we propose an algorithmic framework to simultaneously learn the vector field and Lyapunov functions for unknown nonlinear systems, using a limited amount of data sampled across the state space and along the trajectories at a relatively low sampling frequency. The proposed framework builds upon recently developed high-accuracy Koopman generator learning for capturing transient system transitions and physics-informed neural networks for training Lyapunov functions. We show that the learned Lyapunov functions can be formally verified using a satisfiability modulo theories (SMT) solver and provide less conservative estimates of the region of attraction compared to existing methods.