Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866908416670171136 |
|---|---|
| author | Liu, Jun Fitzsimmons, Maxwell |
| author_facet | Liu, Jun Fitzsimmons, Maxwell |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_18171 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions Liu, Jun Fitzsimmons, Maxwell Systems and Control Dynamical Systems Optimization and Control 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. |
| title | Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions |
| topic | Systems and Control Dynamical Systems Optimization and Control |
| url | https://arxiv.org/abs/2506.18171 |