A Recurrence-based Direct Method for Stability Analysis and GPU-based Verification of Non-monotonic Lyapunov Functions

Lyapunov's direct method is a powerful tool that provides a rigorous framework for stability analysis and control design for dynamical systems. A critical step that enables the application of the method is the existence of a Lyapunov function V -a function whose value monotonically decreases along the trajectories of the dynamical system. Unfortunately, finding a Lyapunov function is often tricky and requires ingenuity, domain knowledge, or significant computational power. At the core of this challenge is the fact that the method requires every sub-level set of V (V-<= c) to be forward invariant, thus implicitly coupling the geometry of V-<= c and the trajectories of the system. In this paper, we seek to disentangle this dependence by developing a direct method that substitutes the concept of invariance with the more flexible notion of recurrence. A set is (iota-)recurrent if every trajectory that starts in the set returns to it (within iota seconds). We show that, under mild conditions, the recurrence of sub-level sets V-<= c is sufficient to guarantee stability and introduce the appropriate stronger notions to obtain asymptotic stability and exponential stability. We further provide a GPU-based algorithm to verify whether V satisfies such recurrence conditions up to an arbitrarily small neighborhood of the equilibrium.