Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions

TL;DR

This paper introduces a symbolic reduction approach for the formal synthesis of global polynomial Lyapunov functions, improving efficiency and robustness in stability verification of polynomial dynamical systems.

Contribution

It develops algebraic constraints and symbolic reduction rules for Lyapunov functions, enabling more effective synthesis and stability analysis via SMT solving.

Findings

Symbolic reduction simplifies Lyapunov candidate functions.

The approach enables efficient stability verification using SMT.

It can disprove global stability through instability conditions.

Abstract

We investigate the formal synthesis of global polynomial Lyapunov functions for polynomial vector fields. We establish that a sign-definite polynomial must satisfy specific algebraic constraints, which we leverage to develop a set of straightforward symbolic reduction rules. These rules can be recursively applied to symbolically simplify the Lyapunov candidate, enabling more efficient and robust discovery of Lyapunov functions via optimization or satisfiability modulo theories (SMT) solving. In many cases, without such simplification, finding a valid Lyapunov function is often infeasible. When strict Lyapunov functions are unavailable, we design synthesis procedures for finding weak Lyapunov functions to verify global asymptotic stability using LaSalle's invariance principle. Finally, we encode instability conditions for Lyapunov functions and develop SMT procedures to disprove global asymptotic stability. Through a series of examples, we demonstrate that the proposed symbolic reduction, LaSalle-type conditions, and instability tests allow us to efficiently solve many cases that would otherwise be challenging.