Synthesis of Lyapunov Functions using Formal Verification
Recent employments of SMT solvers within the Lyapunov function synthesis provided effective tools for automated construction of Lyapunov functions alongside with sound computer-assisted certificates. The main benefit of the suggested approach is the formal correctness and elimination of the numerical uncertainty. In the present work, we extend the SMT-based synthesis approach for wider classes of continuous and discrete-time systems. Additionally, we address constructions of Lyapunov functions for state-dependent switching systems. We illustrate our approach by means of various examples from the control systems literature.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Formally Verified Physics-Informed Neural Control Lyapunov Functions
Control Lyapunov functions are a central tool in the design and analysis of stabilizing controllers for nonlinear systems. Constructing such functions, however, remains a significant challenge. In this paper, we investig…
Analytical Lyapunov Function Discovery: An RL-based Generative Approach
Despite advances in learning-based methods, finding valid Lyapunov functions for nonlinear dynamical systems remains challenging. Current neural network approaches face two main issues: challenges in scalable verificatio…
Reinforcement Learning (RL)validSymbolic Reduction for Formal Synthesis of Global Lyapunov Functions
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 dev…
Design SynthesisvalidFossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models
This paper presents Fossil 2.0, a new major release of a software tool for the synthesis of certificates (e.g., Lyapunov and barrier functions) for dynamical systems modelled as ordinary differential and difference equat…
Formal Synthesis of Lyapunov Neural Networks
We propose an automatic and formally sound method for synthesising Lyapunov functions for the asymptotic stability of autonomous non-linear systems. Traditional methods are either analytical and require manual effort or …