arXiv subjects

Ruikun Zhou

Publications and source records attributed to Ruikun Zhou.

18 recordsLinked to original sources

arXiv2026

Patching Control Lyapunov Barrier Functions for Temporal Logic Specifications with Bounded Controls

We propose an abstraction-free framework for controller synthesis for continuous-time dynamical systems subject to Linear Temporal Logic (LTL) specifications and bounded control inputs. The proposed method combines the sequential decomposition of LTL tasks with the use of formally certified Control Lyapunov-Barrier Functions (CLBFs). By formulating local specifications as a sequence of safe-stabilization problems, we systematically approximate and patch the winning sets of the decomposed subtasks. The satisfaction of these local constraints is guaranteed by the offline-computed level sets of the CLBFs. As a result, our framework yields formally verified switching feedback controllers that enable efficient online planning and dynamic re-planning. This ensures robust continuous specification satisfaction in the presence of state perturbations, avoiding the explicit state-space abstractions commonly required in the literature. The approach is validated through numerical simulations and a hardware demonstration on a Crazyflie quadrotor.

eess.SY↗

arXiv2025

Safe Domains of Attraction for Discrete-Time Nonlinear Systems: Characterization and Verifiable Neural Network Estimation

Analysis of nonlinear autonomous systems typically involves estimating domains of attraction, which have been a topic of extensive research interest for decades. Despite that, accurately estimating domains of attraction for nonlinear systems remains a challenging task, where existing methods are conservative or limited to low-dimensional systems. The estimation becomes even more challenging when accounting for state constraints. In this work, we propose a framework to accurately estimate safe (state-constrained) domains of attraction for discrete-time autonomous nonlinear systems. In establishing this framework, we first derive a new Zubov equation, whose solution corresponds to the exact safe domain of attraction. The solution to the aforementioned Zubov equation is shown to be unique and continuous over the whole state space. We then present a physics-informed approach to approximating the solution of the Zubov equation using neural networks. To obtain certifiable estimates of the domain of attraction from the neural network approximate solutions, we propose a verification framework that can be implemented using standard verification tools (e.g., $\alpha,\!\beta$-CROWN and dReal). To illustrate its effectiveness, we demonstrate our approach through numerical examples concerning nonlinear systems with state constraints.

eess.SY↗

arXiv2025

Stability of Jordan Recurrent Neural Network Estimator

State estimation refers to determining the states of a dynamical system that starts from a noisy initial condition and evolves under process noise, based on noisy measurements and a known system model. For linear dynamical systems with white Gaussian noises of known mean and variance, Kalman filtering is a well-known method that leads to stable error dynamics for detectable systems. There are some non-optimal extensions to nonlinear systems. Recent work has used neural networks to develop estimators for nonlinear systems that optimize a criterion. Stability of the error dynamics is even more important than optimality. Jordan recurrent neural networks (JRNs) have a structure that mimics that of a dynamical system and are thus appealing for estimator design. We show that a JRN performs better than an extended Kalman filter(EKF) and unscented Kalman filter(UKF) for several examples. The main contribution of this paper is an input-to-state stability analysis of the error dynamics of JRNs. The stability of the error dynamics of several examples is shown.

math.OC↗

arXiv2024

Learning Koopman-based Stability Certificates for Unknown Nonlinear Systems

Koopman operator theory has gained significant attention in recent years for identifying discrete-time nonlinear systems by embedding them into an infinite-dimensional linear vector space. However, providing stability guarantees while learning the continuous-time dynamics, especially under conditions of relatively low observation frequency, remains a challenge within the existing Koopman-based learning frameworks. To address this challenge, we propose an algorithmic framework to simultaneously learn the vector field and Lyapunov functions for unknown nonlinear systems, using a limited amount of data sampled across the state space and along the trajectories at a relatively low sampling frequency. The proposed framework builds upon recently developed high-accuracy Koopman generator learning for capturing transient system transitions and physics-informed neural networks for training Lyapunov functions. We show that the learned Lyapunov functions can be formally verified using a satisfiability modulo theories (SMT) solver and provide less conservative estimates of the region of attraction compared to existing methods.

eess.SY↗

arXiv2024

Data-driven optimal control of unknown nonlinear dynamical systems using the Koopman operator

Nonlinear optimal control is vital for numerous applications but remains challenging for unknown systems due to the difficulties in accurately modelling dynamics and handling computational demands, particularly in high-dimensional settings. This work develops a theoretically certifiable framework that integrates a modified Koopman operator approach with model-based reinforcement learning to address these challenges. By relaxing the requirements on observable functions, our method incorporates nonlinear terms involving both states and control inputs, significantly enhancing system identification accuracy. Moreover, by leveraging the power of neural networks to solve partial differential equations (PDEs), our approach is able to achieving stabilizing control for high-dimensional dynamical systems, up to 9-dimensional. The learned value function and control laws are proven to converge to those of the true system at each iteration. Additionally, the accumulated cost of the learned control closely approximates that of the true system, with errors ranging from $10^{-5}$ to $10^{-3}$.

eess.SY↗

arXiv2024

Resolvent-Type Data-Driven Learning of Generators for Unknown Continuous-Time Dynamical Systems

A semigroup characterization, or equivalently, a characterization by the generator, is a classical technique used to describe continuous-time nonlinear dynamical systems. In the realm of data-driven learning for an unknown nonlinear system, one must estimate the generator of the semigroup of the system's transfer operators (also known as the semigroup of Koopman operators) based on discrete-time observations and verify convergence to the true generator in an appropriate sense. As the generator encodes essential instantaneous transitional information of the system, challenges arise for some existing methods that rely on accurately estimating the time derivatives of the state with constraints on the observation rate. Recent literature develops a technique that avoids the use of time derivatives by employing the logarithm of a Koopman operator. However, the validity of this method has been demonstrated only within a restrictive function space and requires knowledge of the operator's spectral properties. In this paper, we propose a resolvent-type method for learning the system generator to relax the requirements on the observation frequency and overcome the constraints of taking operator logarithms. We also provide numerical examples to demonstrate its effectiveness in applications of system identification and constructing Lyapunov functions.

math.DS↗

arXiv2024

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 investigate physics-informed learning and formal verification of neural network control Lyapunov functions. These neural networks solve a transformed Hamilton-Jacobi-Bellman equation, augmented by data generated using Pontryagin's maximum principle. Similar to how Zubov's equation characterizes the domain of attraction for autonomous systems, this equation characterizes the null-controllability set of a controlled system. This principled learning of neural network control Lyapunov functions outperforms alternative approaches, such as sum-of-squares and rational control Lyapunov functions, as demonstrated by numerical examples. As an intermediate step, we also present results on the formal verification of quadratic control Lyapunov functions, which, aided by satisfiability modulo theories solvers, can perform surprisingly well compared to more sophisticated approaches and efficiently produce global certificates of null-controllability.

eess.SY↗

arXiv2024

Stochastic Reinforcement Learning with Stability Guarantees for Control of Unknown Nonlinear Systems

Designing a stabilizing controller for nonlinear systems is a challenging task, especially for high-dimensional problems with unknown dynamics. Traditional reinforcement learning algorithms applied to stabilization tasks tend to drive the system close to the equilibrium point. However, these approaches often fall short of achieving true stabilization and result in persistent oscillations around the equilibrium point. In this work, we propose a reinforcement learning algorithm that stabilizes the system by learning a local linear representation ofthe dynamics. The main component of the algorithm is integrating the learned gain matrix directly into the neural policy. We demonstrate the effectiveness of our algorithm on several challenging high-dimensional dynamical systems. In these simulations, our algorithm outperforms popular reinforcement learning algorithms, such as soft actor-critic (SAC) and proximal policy optimization (PPO), and successfully stabilizes the system. To support the numerical results, we provide a theoretical analysis of the feasibility of the learned algorithm for both deterministic and stochastic reinforcement learning settings, along with a convergence analysis of the proposed learning algorithm. Furthermore, we verify that the learned control policies indeed provide asymptotic stability for the nonlinear systems.

eess.SY↗

arXiv2024

A Model-Free Kullback-Leibler Divergence Filter for Anomaly Detection in Noisy Data Series

We propose a Kullback-Leibler Divergence (KLD) filter to extract anomalies within data series generated by a broad class of proximity sensors, along with the anomaly locations and their relative sizes. The technique applies to devices commonly used in engineering practice, such as those mounted on mobile robots for non-destructive inspection of hazardous or other environments that may not be directly accessible to humans. The raw data generated by this class of sensors can be challenging to analyze due to the prevalence of noise over the signal content. The proposed filter is built to detect the difference of information content between data series collected by the sensor and baseline data series. It is applicable in a model-based or model-free context. The performance of the KLD filter is validated in an industrial-norm setup and benchmarked against a peer industrially-adopted algorithm.

eess.SP↗

arXiv2024

Koopman-Based Learning of Infinitesimal Generators without Operator Logarithm

The Koopman operator has gained significant attention in recent years for its ability to verify evolutionary properties of continuous-time nonlinear systems by lifting state variables into an infinite-dimensional linear vector space. The challenge remains in providing estimations for transitional properties pertaining to the system's vector fields based on discrete-time observations. To retrieve such infinitesimal system transition information, leveraging the structure of Koopman operator learning, current literature focuses on developing techniques free of time derivatives through the use of the Koopman operator logarithm. However, the soundness of these methods has so far been demonstrated only for maintaining effectiveness within a restrictive function space, together with knowledge of the operator spectrum properties. To better adapt to the practical applications in learning and control of unknown systems, we propose a logarithm-free technique for learning the infinitesimal generator without disrupting the Koopman operator learning framework. This approach claims compatibility with other system verification tools using the same set of training data. We provide numerical examples to demonstrate its effectiveness in applications of system identification and stability prediction.

math.DS↗

arXiv2024

Compositionally Verifiable Vector Neural Lyapunov Functions for Stability Analysis of Interconnected Nonlinear Systems

While there has been increasing interest in using neural networks to compute Lyapunov functions, verifying that these functions satisfy the Lyapunov conditions and certifying stability regions remain challenging due to the curse of dimensionality. In this paper, we demonstrate that by leveraging the compositional structure of interconnected nonlinear systems, it is possible to verify neural Lyapunov functions for high-dimensional systems beyond the capabilities of current satisfiability modulo theories (SMT) solvers using a monolithic approach. Our numerical examples employ neural Lyapunov functions trained by solving Zubov's partial differential equation (PDE), which characterizes the domain of attraction for individual subsystems. These examples show a performance advantage over sums-of-squares (SOS) polynomial Lyapunov functions derived from semidefinite programming.

eess.SY↗

arXiv2024

LyZNet: A Lightweight Python Tool for Learning and Verifying Neural Lyapunov Functions and Regions of Attraction

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. The repository of the tool can be found at https://git.uwaterloo.ca/hybrid-systems-lab/lyznet.

eess.SY↗

arXiv2024

Physics-Informed Neural Network Policy Iteration: Algorithms, Convergence, and Verification

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.

eess.SY↗

arXiv2023

Physics-Informed Neural Network Lyapunov Functions: PDE Characterization, Learning, and Verification

We provide a systematic investigation of using physics-informed neural networks to compute Lyapunov functions. We encode Lyapunov conditions as a partial differential equation (PDE) and use this for training neural network Lyapunov functions. We analyze the analytical properties of the solutions to the Lyapunov and Zubov PDEs. In particular, we show that employing the Zubov equation in training neural Lyapunov functions can lead to approximate regions of attraction close to the true domain of attraction. We also examine approximation errors and the convergence of neural approximations to the unique solution of Zubov's equation. We then provide sufficient conditions for the learned neural Lyapunov functions that can be readily verified by satisfiability modulo theories (SMT) solvers, enabling formal verification of both local stability analysis and region-of-attraction estimates in the large. Through a number of nonlinear examples, ranging from low to high dimensions, we demonstrate that the proposed framework can outperform traditional sums-of-squares (SOS) Lyapunov functions obtained using semidefinite programming (SDP).

math.OC↗

arXiv2023

Learning Regions of Attraction in Unknown Dynamical Systems via Zubov-Koopman Lifting: Regularities and Convergence

The estimation for the region of attraction (ROA) of an asymptotically stable equilibrium point is crucial in the analysis of nonlinear systems. There has been a recent surge of interest in estimating the solution to Zubov's equation, whose non-trivial sub-level sets form the exact ROA. In this paper, we propose a lifting approach to map observable data into an infinite-dimensional function space, which generates a flow governed by the proposed `Zubov-Koopman' operators. By learning a Zubov-Koopman operator over a fixed time interval, we can indirectly approximate the solution to Zubov's equation through iterative application of the learned operator on certain functions. We also demonstrate that a transformation of such an approximator can be readily utilized as a near-maximal Lyapunov function. We approach our goal through a comprehensive investigation of the regularities of Zubov-Koopman operators and their associated quantities. Based on these findings, we present an algorithm for learning Zubov-Koopman operators that exhibit strong convergence to the true operator. We show that this approach reduces the amount of required data and can yield desirable estimation results, as demonstrated through numerical examples.

math.DS↗

arXiv2023

Harmonic Control Lyapunov Barrier Functions for Constrained Optimal Control with Reach-Avoid Specifications

This paper introduces harmonic control Lyapunov barrier functions (harmonic CLBF) that aid in constrained control problems such as reach-avoid problems. Harmonic CLBFs exploit the maximum principle that harmonic functions satisfy to encode the properties of control Lyapunov barrier functions (CLBFs). As a result, they can be initiated at the start of an experiment rather than trained based on sample trajectories. The control inputs are selected to maximize the inner product of the system dynamics with the steepest descent direction of the harmonic CLBF. Numerical results are presented with four different systems under different reach-avoid environments. Harmonic CLBFs show a significantly low risk of entering unsafe regions and a high probability of entering the goal region.

math.OC↗

arXiv2023

Towards Learning and Verifying Maximal Neural Lyapunov Functions

The search for Lyapunov functions is a crucial task in the analysis of nonlinear systems. In this paper, we present a physics-informed neural network (PINN) approach to learning a Lyapunov function that is nearly maximal for a given stable set. A Lyapunov function is considered nearly maximal if its sub-level sets can be made arbitrarily close to the boundary of the domain of attraction. We use Zubov's equation to train a maximal Lyapunov function defined on the domain of attraction. Additionally, we propose conditions that can be readily verified by satisfiability modulo theories (SMT) solvers for both local and global stability. We provide theoretical guarantees on the existence of maximal Lyapunov functions and demonstrate the effectiveness of our computational approach through numerical examples.

math.OC↗

arXiv2022

Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees

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 nonlinear controller. The SMT solver then verifies that the candidate Lyapunov function indeed satisfies the Lyapunov conditions. We provide theoretical guarantees of the proposed learning framework in terms of the closed-loop stability for the unknown nonlinear system. We illustrate the effectiveness of the approach with a set of numerical experiments.

eess.SY↗