A constructive converse Lyapunov theorem on exponential stability

Closed physical systems eventually come to rest, the reason being that due to friction of some kind they continuously lose energy. The mathematical extension of this principle is the concept of a Lyapunov function. A Lyapunov function for a dynamical system, of which the dynamics are modelled by an ordinary differential equation (ODE), is a function that is decreasing along any trajectory of the system and with exactly one local minimum. This implies that the system must eventually come to rest at this minimum. Although it has been known for over 50 years that the asymptotic stability of an ODE's equilibrium is equivalent to the existence of a Lyapunov function for the ODE, there has been no constructive method for non-local Lyapunov functions, except in special cases. Recently, a novel method to construct Lyapunov functions for ODEs via linear programming was presented [5], [6], which includes an algorithmic description of how to derive a linear program for a continuous autonomous ODE, such that a Lyapunov function can be constructed from any feasible solution of this linear program. We will show how to choose the free parameters of this linear program, dependent on the ODE in question, so that it will have a feasible solution if the equilibrium at the origin is exponentially stable. This leads to the first constructive converse Lyapunov theorem in the theory of dynamical systems/ODEs.