  In this paper, we examine linear programming (LP) based relaxations for
synthesizing polynomial Lyapunov functions to prove the stability of polynomial
ODEs. A common approach to Lyapunov function synthesis starts from a desired
parametric polynomial form of the polynomial Lyapunov function. Subsequently,
we encode the positive-definiteness of the function, and the
negative-definiteness of its derivative over the domain of interest. Therefore,
the key primitives for this encoding include: (a) proving that a given
polynomial is positive definite over a domain of interest, and (b) encoding the
positive definiteness of a given parametric polynomial, as a constraint on the
unknown parameters. We first examine two classes of relaxations for proving
polynomial positivity: relaxations by sum-of-squares (SOS) programs, against
relaxations that produce linear programs. We compare both types of relaxations
by examining the class of polynomials that can be shown to be positive in each
case. Next, we present a progression of increasingly more powerful LP
relaxations based on expressing the given polynomial in its Bernstein form, as
a linear combination of Bernstein polynomials. The well-known bounds on
Bernstein polynomials over the unit box help us formulate increasingly precise
LP relaxations that help us establish the positive definiteness of a polynomial
over a bounded domain. Subsequently, we show how these LP relaxations can be
used to search for Lyapunov functions for polynomial ODEs by formulating LP
instances. We compare our approaches to synthesizing Lyapunov functions with
approaches based on SOS programming relaxations.
