In this paper, we describe a lightweight Python framework that provides integrated learning and verification of neural Lyapunov functions for stability analysis. The proposed tool, named LyZNet, learns neural Lyapunov functions using physics-informed neural networks (PINNs) to solve Zubov’s equation and verifies them using satisfiability modulo theories (SMT) solvers. What distinguishes this tool from others in the literature is its ability to provide verified regions of attraction close to the domain of attraction. This is achieved by encoding Zubov’s partial differential equation (PDE) into the PINN approach. By embracing the non-convex nature of the underlying optimization problems, we demonstrate that in cases where convex optimization, such as semidefinite programming, fails to capture the domain of attraction, our neural network framework proves more successful. The tool also offers automatic decomposition of coupled nonlinear systems into a network of low-dimensional subsystems for compositional verification. We illustrate the tool’s usage and effectiveness with several numerical examples, including both non-trivial low-dimensional nonlinear systems and high-dimensional systems.

In this paper, we present physics-informed neural networks (PINNs) for the analysis and control of nonlinear systems. PINNs are designed to solve partial differential equations (PDEs). We demonstrate their applications in various challenging computational tasks in systems and control, including computing Lyapunov functions, regions of attraction, and optimal value functions and controllers for nonlinear systems. Additionally, we introduce LyZNet, a tool that combines physics-informed learning with formal verification to ensure the solutions provided by PINNs meet formal guarantees. We provide theoretical results and demonstrate with numerical examples of both low- and high-dimensional nonlinear systems to showcase the effectiveness of the proposed framework.

Solving nonlinear optimal control problems is a challenging task, particularly for high-dimensional problems. We propose algorithms for model-based policy iterations to solve nonlinear optimal control problems with convergence guarantees. The main component of our approach is an iterative procedure that utilizes neural approximations to solve linear partial differential equations (PDEs), ensuring convergence. We present two variants of the algorithms. The first variant formulates the optimization problem as a linear least square problem, drawing inspiration from extreme learning machine (ELM) for solving PDEs. This variant efficiently handles low-dimensional problems with high accuracy. The second variant is based on a physics-informed neural network (PINN) for solving PDEs and has the potential to address high-dimensional problems. We demonstrate that both algorithms outperform traditional approaches, such as Galerkin methods, by a significant margin. We provide a theoretical analysis of both algorithms in terms of convergence of neural approximations towards the true optimal solutions in a general setting. Furthermore, we employ formal verification techniques to demonstrate the verifiable stability of the resulting controllers.

The vast majority of convergence rates analysis for stochastic gradient methods in the literature focus on convergence in expectation, whereas trajectory-wise almost sure convergence is clearly important to ensure that any instantiation of the stochastic algorithms would converge with probability one. Here we provide a unified almost sure convergence rates analysis for stochastic gradient descent (SGD), stochastic heavy-ball (SHB), and stochastic Nesterov's accelerated gradient (SNAG) methods. We show, for the first time, that the almost sure convergence rates obtained for these stochastic gradient methods on strongly convex functions, are arbitrarily close to their optimal convergence rates possible. For non-convex objective functions, we not only show that a weighted average of the squared gradient norms converges to zero almost surely, but also the last iterates of the algorithms. We further provide last-iterate almost sure convergence rates analysis for stochastic gradient methods on general convex smooth functions, in contrast with most existing results in the literature that only provide convergence in expectation for a weighted average of the iterates. The last-iterate almost sure convergence results also enable us to obtain almost sure avoidance of any strict saddle manifold by stochastic gradient methods with or without momentum. To the best of our knowledge, this is the first time such results are obtained for SHB and SNAG methods.

The vast majority of convergence rates analysis for stochastic gradient methods in the literature focus on convergence in expectation, whereas trajectory-wise almost sure convergence is clearly important to ensure that any instantiation of the stochastic algorithms would converge with probability one. Here we provide a unified almost sure convergence rates analysis for stochastic gradient descent (SGD), stochastic heavy-ball (SHB), and stochastic Nesterov’s accelerated gradient (SNAG) methods. We show, for the first time, that the almost sure convergence rates obtained for these stochastic gradient methods on strongly convex functions, are arbitrarily close to their optimal convergence rates possible. For non-convex objective functions, we not only show that a weighted average of the squared gradient norms converges to zero almost surely, but also the last iterates of the algorithms. We further provide last-iterate almost sure convergence rates analysis for stochastic gradient methods on weakly convex smooth functions, in contrast with most existing results in the literature that only provide convergence in expectation for a weighted average of the iterates.

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 with provable guarantees. 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 nonlinear controller. The SMT solver verifies the candidate Lyapunov function satisfies the Lyapunov conditions. We further provide theoretical guarantees of the proposed learning framework and show that the obtained Lyapunov function indeed verifies for the unknown nonlinear system under mild assumptions. We illustrate the effectiveness of the results with a few numerical experiments.

This work addresses the problem of aperiodically sampled control for the networked Takagi-Sugeno (T-S) fuzzy systems, where the aperiodically sampled input is generated by a periodic sampler and an event-triggered mechanism (ETM). The purpose of ETM is used to reduce the computational and communication burdens. For guaranteeing controller robustness, the practical stability of T-S fuzzy systems is considered by using the Lyapunov method and linear matrix inequality (LMI) technique. As one of the most powerful inequalities for deriving stability criteria using LMIs, Jensen's inequality has recently been improved by various authors for the stability analysis of delayed systems. However, these results are conservative to obtain lower bounds for integrals with an exponential term. Inspired by this, improved integral inequalities are derived in this work, and they are applied to obtain practical stability criteria for aperiodically sampled control. Finally, a numerical example on flight control of a helicopter is given to illustrate the effectiveness of the obtained practical stability criteria. Furthermore, the effectiveness of the improved Jensen inequalities on the exponential stability criteria is illustrated by numerical comparisons.

Practical stability analysis for delayed systems is discussed. Weak practical stability conditions are derived by using Halanay’s inequality and the Lyapunov method. The results are applied to address the problem of practical stability of a power system over a delay-induced communication network. An event-detection-based control scheme is proposed to reduce the communication burdens. Based on the obtained practical stability conditions and the proposed event-detection scheme, sufficient practical stability conditions for load frequency control of a networked power system are given. Furthermore, a new design approach to the event-detection-based controller is presented. Finally, a numerical simulation is given to show the effectiveness and advantage of the obtained results.

This paper proposes an online control framework for mobile robots to satisfy a complex mission given in the form of linear temporal logic (LTL) without colliding with moving obstacles in the environment. The proposed framework consists of three modules named the static planner, the local collision avoidance, and the patcher. The static planner is synthesized by solving a parity game for a finite abstraction of the robot model based on a world map with static obstacles to fulfill the LTL task. The local collision avoidance module computes a set of safe controls that guarantees a safe distance between the moving objects. Both of the modules can be rigorously computed offline only once via formal methods. The patcher is activated whenever a moving obstacle is detected and modifies the static plan online for a short horizon by using only provably safe controls. The resulting modified strategy can guarantee collision-free motion without losing the ability to satisfy the LTL task. As opposed to using assume-guarantee type of LTL tasks, the proposed framework can handle the situations where obstacle movement is unpredictable.

In this article, the problem of flight control for a two-degree-of-freedom helicopter system is studied. Since the helicopter is a multiinput, multioutput nonlinear control system, a Takagi–Sugeno (T–S) fuzzy model is applied to approximate the system. All submodels of the new T–S fuzzy model contain constant terms due to the nonlinear characteristics of the helicopter system. In this article, sampled-data control is considered and the sampled data are transmitted to the system over a communication network. A large amount of sampled data transmitted over the network can significantly increase the computational and communication burdens for the network with a limited bandwidth. To overcome this difficulty, an event-triggered mechanism is introduced. In order to validly control the T–S fuzzy system, a fuzzy proportional integral-derivative (PID) controller is designed based on the Lyapunov method and practical stability criteria, which are obtained by using improved integral inequalities and the linear matrix inequality technique. Finally, a numerical example is given to show the effectiveness of the obtained results.

We propose a novel technique for improving the stochastic gradient descent (SGD) method to train deep networks, which we term pbSGD. The proposed pbSGD method simply raises the stochastic gradient to a certain power elementwise during iterations and introduces only one additional parameter, namely, the power exponent (when it equals to 1, pbSGD reduces to SGD). We further propose pbSGD with momentum, which we term pbSGDM. The main results of this paper present comprehensive experiments on popular deep learning models and benchmark datasets. Empirical results show that the proposed pbSGD and pbSGDM obtain faster initial training speed than adaptive gradient methods, comparable generalization ability with SGD, and improved robustness to hyper-parameter selection and vanishing gradients. pbSGD is essentially a gradient modifier via a nonlinear transformation. As such, it is orthogonal and complementary to other techniques for accelerating gradient-based optimization such as learning rate schedules. Finally, we show convergence rate analysis for both pbSGD and pbSGDM methods. The theoretical rates of convergence match the best known theoretical rates of convergence for SGD and SGDM methods on nonconvex functions.

The stability problem is studied for hybrid systems with delays in this paper. Based on Lyapunov–Razumikhin approach, a novel theorem is presented for such system with the characteristic of homogeneity so that the system is globally preasymptotically stable. In particular, under the homogeneous assumption, we are able to obtain some rather weak conditions compared with general nonhomogeneous hybrid systems in this paper. Finally, two illustrative numerical examples are presented to demonstrate the applicability and the effectiveness of our theorems.

This paper presents ROCS, an algorithmic control synthesis tool for nonlinear dynamical systems. Different from other formal control synthesis tools, it guarantees to generate a control strategy with respect to a robustly realizable specification for a nonlinear system. At the core of ROCS is the interval branch-and-bound scheme with a precision control parameter that reflects the robustness of the realizability of the specification. It also supports multiple variable precision control parameters to achieve higher efficiency.

This demo abstract presents ROCS, an algorithmic control synthesis tool for nonlinear dynamical systems. Different from other formal control synthesis tools, it guarantees to generate a control strategy with respect to a robustly realizable specification for a nonlinear system. The functionality and usability of ROCS will be illustrated through examples.

While using temporal logic specifications with motion planning has been heavily researched, the reliance on having an available steering function is impractical and often suited only to basic problems with linear dynamics. This is because a steering function is a solution to an optimal two-point boundary value problem (OBVP); to our knowledge, it is nearly impossible to find an analytic solution to such problems in many cases. Addressing this issue, we have developed a means of combining the asymptotically optimal and probabilistically complete kinodynamic planning algorithm SST* with a local deterministic μ-calculus model checking procedure to create a motion planning algorithm with deterministic μ-calculus specifications that does not rely on a steering function. The procedure involves combining only the most pertinent information from multiple Kripke structures in order to create one abstracted Kripke structure storing the best paths to all possible proposition regions of the state-space. A linear-quadratic regulator (LQR) feedback control policy is then used to track these best paths, effectively connecting the trajectories found from multiple Kripke structures. Simulations demonstrate that it is possible to satisfy a complex liveness specification for infinitely often reaching specified regions of state-space using only forward propagation.

We define robust abstractions for synthesizing provably correct and robust controllers for (possibly infinite) uncertain transition systems. It is shown that robust abstractions are sound in the sense that they preserve robust satisfaction of linear-time properties. We then focus on discrete-time control systems modelled by nonlinear difference equations with inputs and define concrete robust abstractions for them. While most abstraction techniques in the literature for nonlinear systems focus on constructing sound abstractions, we present computational procedures for constructing both sound and approximately complete robust abstractions for general nonlinear control systems without stability assumptions. Such procedures are approximately complete in the sense that, given a concrete discrete-time control system and an arbitrarily small perturbation of this system, there exists a finite transition system that robustly abstracts the concrete system and is abstracted by the slightly perturbed system simultaneously. A direct consequence of this result is that robust control synthesis for discrete-time nonlinear systems and linear-time specifications is robustly decidable. More specifically, if there exists a robust control strategy that realizes a given linear-time specification, we can algorithmically construct a (potentially less) robust control strategy that realizes the same specification. The theoretical results are illustrated with a simple motion planning example.

Abstraction-based, hierarchical approaches to control synthesis from temporal logic specifications for dynamical systems have gained increased popularity over the last decade. Yet various issues commonly encountered and extensively dealt with in control systems have not been adequately discussed in the context of temporal logic control of dynamical systems, such as inter-sample behaviors of a sampled-data system, effects of imperfect state measurements and un-modeled dynamics, and the use of time-discretized models to design controllers for continuous-time dynamical systems. We discuss these issues in this paper. The main motivation is to demonstrate the possibility of accounting for the mismatches between a continuous-time control system and its various types of abstract models used for control synthesis. We do this by incorporating additional robustness measures in the abstract models. Such robustness measures are gained at the price of either increased non-determinism in the abstracted models or relaxed versions of the specification being realized. Under a unified notion of abstraction, we provide concrete means of incorporating these robustness measures and establish results that demonstrate their effectiveness in dealing with the above mentioned issues.

Motivated by designing high-level planners for dynamical systems (such as mobile robots) to achieve complex tasks, we consider the synthesis of switching controllers of nonlinear dynamical systems from metric temporal logic (MTL) specifications. MTL is a popular logic that allows to specify timed properties of real-time reactive systems and hence is appropriate for describing the safe and autonomous operations of robotic systems in an uncertain and possibly adversarial environment. We provide constructive means for computing finite-state abstractions that preserve MTL properties for nonlinear systems, under a weak assumption that these nonlinear systems evolve continuously with respect to their initial conditions. We then provide conditions to ensure that the existence of a discrete strategy (obtained by solving a discrete synthesis problem) guarantees the existence of a switching strategy for controlling the continuous-time dynamical systems to satisfy a given MTL specification. We illustrate the results on a motion planning problem.

Pre-orders on systems are the basis for abstraction based verification of systems. In this paper, we investigate pre-orders for reasoning about stability with respect to inputs of hybrid systems. First, we present a superposition type theorem which gives a characterization of the classical incremental input-to-state stability of continuous systems in terms of the traditional ε-δ definition of stability. We use this as the basis for defining a notion of incremental input-to-state stability of hybrid systems. Next, we present a pre-order on hybrid systems which preserves incremental input-to-state stability, by extending the classical definitions of bisimulation relations on systems with input, with uniform continuity constraints. We show that the uniform continuity is a necessary requirement by exhibiting counter-examples to show that weaker notions of input bisimulation with just continuity requirements do not suffice to preserve stability. Finally, we demonstrate that the definitions are useful, by exhibiting concrete abstraction functions which satisfy the definitions of pre-orders.

We investigate the robustness of reactive control protocols synthesized to guarantee system's correctness with respect to given temporal logic specifications. We consider uncertainties in open finite transition systems due to unmodeled transitions. The resulting robust synthesis problem is formulated as a temporal logic game. In particular, if the specification is in the so-called generalized reactivity [1] fragment of linear temporal logic, so is the augmented specification in the resulting robust synthesis problem. Hence, the robust synthesis problem belongs to the same complexity class with the nominal synthesis problem, and is amenable to polynomial time solvers. Additionally, we discuss reasoning about the effects of different levels of uncertainties on robust synthesizability and demonstrate the results on a simple robot motion planning scenario.