Data-driven stability verification and region of attraction estimation for Koopman-lifted nonlinear systems

This is the authors' abstract. We don't add key points for this paper.

This paper presents a data-driven framework for verifying static state-feedback stabilisers for control-affine nonlinear systems using a Koopman-lifted behavioural representation. The state is embedded into a finite-dimensional observable space, and one-step lifted data matrices are constructed from persistently exciting exploratory trajectories collected under an auxiliary pre-stabilising feedback. To reduce the conservatism associated with global-fit residual bias, a two-stage protocol is introduced. In Stage (i), the exploratory lifted data are used to construct a behavioural representation of a candidate closed loop via the Koopman-lifted extension of Willems’ fundamental lemma, to screen candidate feedback gains. In Stage (ii), dedicated near-equilibrium closed-loop perturbation data are used to identify a local closed-loop Jacobian, from which a quadratic Lyapunov function is computed via a discrete Lyapunov equation. Under the local embedding and residual assumptions, this lifted Lyapunov function induces a local Riemannian contraction metric on the underlying nonlinear manifold. Building on this construction, the paper develops two complementary certificates: a deterministic local Region-of-Attraction inner bound, together with Local Input-to-State Stability margins against unmodelled dynamics, obtained from a local residual bound; and a scenario-certified probabilistic one-step Lyapunov decrease set obtained using the Scenario Approach applied directly to the nonlinear closed-loop dynamics. The framework is validated on an inverted-pendulum benchmark and shown to be competitive with strong baseline controllers while additionally providing explicit stability certificates grounded in measured trajectory data.