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 are numerical but lack of formal soundness. Symbolic computational methods for Lyapunov functions, which are in between, give formal guarantees but are typically semi-automatic because they rely on the user to provide appropriate function templates. We propose a method that finds Lyapunov functions fully automatically$-$using machine learning$-$while also providing formal guarantees$-$using satisfiability modulo theories (SMT). We employ a counterexample-guided approach where a numerical learner and a symbolic verifier interact to construct provably correct Lyapunov neural networks (LNNs). The learner trains a neural network that satisfies the Lyapunov criteria for asymptotic stability over a samples set; the verifier proves via SMT solving that the criteria are satisfied over the whole domain or augments the samples set with counterexamples. Our method supports neural networks with polynomial activation functions and multiple depth and width, which display wide learning capabilities. We demonstrate our method over several non-trivial benchmarks and compare it favourably against a numerical optimisation-based approach, a symbolic template-based approach, and a cognate LNN-based approach. Our method synthesises Lyapunov functions faster and over wider spatial domains than the alternatives, yet providing stronger or equal guarantees.
In this paper we employ SMT solvers to soundly synthesise Lyapunov functions that assert the stability of a given dynamical model. The search for a Lyapunov function is framed as the satisfiability of a second-order logical formula, asking whether there exists a function satisfying a desired specification (stability) for all possible initial conditions of the model. We synthesise Lyapunov functions for linear, non-linear (polynomial), and for parametric models. For non-linear models, the algorithm also determines a region of validity for the Lyapunov function. We exploit an inductive framework…
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 t…
Adaptive Meshing for CPA Lyapunov Function Synthesis
Thomas Lord Department of Mechanical Engineering and Materials Science, Duke University（杜克大学托马斯·劳德机械与材料工程系）；Department of Aeronautics and Astronautics, Stanford University（斯坦福大学航空与航天工程系）
A controller synthesis method for state- and input-constrained nonlinear systems is presented that seeks continuous piecewise affine (CPA) Lyapunov-like functions and controllers simultaneously. Non-convex optimization problems are formulated on triangulated subsets of the admissible states that can be refined to meet primary control objectives, such as stability and safety, alongside secondary performance objectives. A multi-stage design is also given that enlarges the region of attraction (ROA) sequentially while allowing exclusive performance for each stage. A clear boundary for an invarian…
This paper addresses the co-design problem of control inputs and execution decisions for event- and self-triggered controls subject to constraints given by the control Lyapunov function and control barrier function. The proposed approach computes the control input in a way that allows for longer inter-execution intervals, which distinguishes it from many existing event- and self-triggered controllers or control Lyapunov-barrier function controllers. The proposed approach guarantees lower bounds on the minimum inter-execution times. The effectiveness of the proposed approach is demonstrated and…
This paper considers the problem of designing accelerated gradient-based algorithms for optimization and saddle-point problems. The class of objective functions is defined by a generalized sector condition. This class of functions contains strongly convex functions with Lipschitz gradients but also non-convex functions, which allows not only to address optimization problems but also saddle-point problems. The proposed design procedure relies on a suitable class of Lyapunov functions and on convex semi-definite programming. The proposed synthesis allows the design of algorithms that reach the p…
Control Lyapunov functions (CLFs) and control barrier functions (CBFs) are widely used tools for synthesizing controllers subject to stability and safety constraints. Paired with online optimization, they provide stabilizing control actions that satisfy input constraints and avoid unsafe regions of state-space. Designing CLFs and CBFs with rigorous performance guarantees is computationally challenging. To certify existence of control actions, current techniques not only design a CLF/CBF, but also a nominal controller. This can make the synthesis task more expensive, and performance estimation …
In this technical note, we generalize the well-known Lyapunov-based stabilizability and detectability tests for linear time-invariant (LTI) systems to the context of discrete-time (DT) polytopic linear parameter-varying (LPV) systems. To do so, we exploit the mathematical structure of the class of poly-quadratic Lyapunov functions, which enables us to formulate conditions in the form of linear matrix inequalities (LMIs). Our results differ from existing conditions in that we adopt weaker assumptions on the parameter dependence of the controllers/observers and our method does not require explic…
Equivalent Stability Notions, Lyapunov Inequality, and Its Application in Discrete-Time Linear Systems with Stochastic Dynamics Determined by an i.i.d. Process
This paper proposes a framework for automatic formal controller synthesis for general hybrid systems with a subset of safety and reachability specifications. The framework uses genetic programming to automatically co-synthesize controllers and candidate Lyapunov-like functions. These candidate Lyapunov-like functions are used to formally verify the control specification, and their correctness is proven using a Satisfiability Modulo Theories solver. The advantages of this approach are: no restriction is made to polynomial systems, the synthesized controllers are expressed as compact expressions…
We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) for the safety verification of continuous and hybrid dynamical models. The approach is underpinned by an inductive framework: this is structured as a sequential loop between a learner, which manipulates a candidate BC structured as a neural network, and a sound verifier, which either certifies the candidate's validity or generates counter-examples to further guide the learner. We compare the approach against state-of-the-art techniques, over polynomial and non-polynomial dynamical models: t…
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
Stanford University（斯坦福大学）；The Hebrew University of Jerusalem（耶路撒冷希伯来大学）；IT University of Copenhagen（哥本哈根信息技术大学）；Google（谷歌公司）；GE Aerospace Research（GE航空航天研究院）
Max Planck Institute for Intelligent Systems（马克斯·普朗克智能系统研究所）；ETH Zürich（苏黎世联邦理工学院）；Google Research（谷歌研究院）
Learning controllers merely based on a performance metric has been proven effective in many physical and non-physical tasks in both control theory and reinforcement learning. However, in practice, the controller must guarantee some notion of safety to ensure that it does not harm either the agent or the environment. Stability is a crucial notion of safety, whose violation can certainly cause unsafe behaviors. Lyapunov functions are effective tools to assess stability in nonlinear dynamical systems. In this paper, we combine an improving Lyapunov function with automatic controller synthesis in …
Sandia National Laboratories（桑迪亚国家实验室）；Clemson University（克莱姆森大学）；Georgia Institute of Technology（佐治亚理工学院）
We consider a class of nonlinear control synthesis problems where the underlying mathematical models are not explicitly known. We propose a data-driven approach to stabilize the systems when only sample trajectories of the dynamics are accessible. Our method is founded on the density function based almost everywhere stability certificate that is dual to the Lyapunov function for dynamic systems. Unlike Lyapunov based methods, density functions lead to a convex formulation for a joint search of the control strategy and the stability certificate. This type of convex problem can be solved efficie…
Polyhedral Lyapunov functions can approximate any norm arbitrarily well. Because of this, they are used to study the stability of linear time varying and linear parameter varying systems without being conservative. However, the computational cost associated with using them grows unbounded as the size of their representation increases. Finding them is also a hard computational problem. Here we present an algorithm that attempts to find polyhedral functions while keeping the size of the representation fixed, to limit computational costs. We do this by measuring the gap from contraction for a giv…
This paper studies control synthesis for a general class of nonlinear, control-affine dynamical systems under additive disturbances and state-estimation errors. We enforce forward invariance of static and dynamic safe sets and convergence to a given goal set within a user-defined time in the presence of input constraints. We use robust variants of control barrier functions (CBF) and fixed-time control Lyapunov functions (FxT-CLF) to incorporate a class of additive disturbances in the system dynamics, and state-estimation errors. To solve the underlying constrained control problem, we formulate…
Analytical Lyapunov Function Discovery: An RL-based Generative Approach
Department of Electrical and Computer Engineering, UC San Diego, La Jolla, United States（加州大学圣地亚哥分校电子与计算机工程系）；Swiss Federal Institute of Technology in Lausanne（洛桑联邦理工学院）
In this paper, we propose a formal controller synthesis approach for integrating a population of plug-in electric vehicles in frequency regulation of power systems. This approach is the first application of formal methods to the smart grids in particular to the frequency regulation of power systems. We design and simulate a novel symbolic controller for the Great Britain power system. The proposed controller enhances the frequency response behaviour of the system when encountered with a large outage event. The symbolic controller guarantees the settlement of the after-event's frequency in the …
Learning for control of dynamical systems with formal guarantees remains a challenging task. This paper proposes a learning framework to simultaneously stabilize an unknown nonlinear system with a neural controller and learn a neural Lyapunov function to certify a region of attraction (ROA) for the closed-loop system. The algorithmic structure consists of two neural networks and a satisfiability modulo theories (SMT) solver. The first neural network is responsible for learning the unknown dynamics. The second neural network aims to identify a valid Lyapunov function and a provably stabilizing …
Patching Control Lyapunov Barrier Functions for Temporal Logic Specifications with Bounded Controls
Massachusetts Institute of Technology（麻省理工学院）；University of Waterloo（滑铁卢大学）；MacLean Engineering & Marketing Co. Limited（麦克林工程与营销有限公司）；Hong Kong University of Science and Technology (Guangzhou)（香港科技大学（广州））
We propose a counterexample-guided inductive synthesis framework for the formal synthesis of closed-form sampled-data controllers for nonlinear systems to meet STL specifications over finite-time trajectories. Rather than stating the STL specification for a single initial condition, we consider an (infinite and bounded) set of initial conditions. Candidate solutions are proposed using genetic programming, which evolves controllers based on a finite number of simulations. Subsequently, the best candidate is verified using reachability analysis; if the candidate solution does not satisfy the spe…
