arXiv subjects

Yiming Meng

Publications and source records attributed to Yiming Meng.

At least 19 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↗

arXiv2026

Characterization of Safe Stabilization and Control Lyapunov-Barrier Functions via Zubov Equation Formulation

Design and analysis of stabilizing controllers with safety guarantees for nonlinear systems have received considerable attention in recent years. Control Lyapunov-barrier functions (CLBFs) provide a powerful framework for simultaneously ensuring stability and safety; however, their construction for nonlinear systems remains challenging. To address this issue, we build on recent advances in PDE-based characterizations of control Lyapunov functions and Lyapunov-barrier functions for autonomous systems, and propose a succinct Zubov-HJB PDE formulation for safe stabilization of nonlinear control-affine systems under a common compatibility assumption. We further show that the viscosity solution of this PDE yields a maximal CLBF, enabling (not necessarily continuous) feedback synthesis with stability and safety guarantees. In light of recent advances in neural-network-based methods for solving Zubov-type PDEs, this theoretical framework also provides a natural interface to emerging numerical approaches.

math.DS↗

arXiv2025

Towards Learning and Verifying Maximal Lyapunov-Barrier Functions with a Zubov PDE Formulation

Verifying stability and safety guarantees for nonlinear systems has received considerable attention in recent years. This property serves as a fundamental building block for specifying more complex system behaviors and control objectives. However, estimating the domain of attraction under safety constraints and constructing a Lyapunov-barrier function remain challenging tasks for nonlinear systems. To address this problem, we propose a Zubov PDE formulation with a Dirichlet boundary condition for autonomous nonlinear systems and show that a physics-informed neural network solution, once formally verified, can serve as a Lyapunov-barrier function that jointly certifies stability and safety. This approach extends existing converse Lyapunov-barrier theorems by introducing a PDE-based framework with boundary conditions defined on the safe set, yielding a near-optimal certified under-approximation of the true safe domain of attraction.

math.DS↗

arXiv2025

Reachable Predictive Control: A Novel Control Algorithm for Nonlinear Systems with Unknown Dynamics and its Practical Applications

This paper proposes an algorithm capable of driving a system to follow a piecewise linear trajectory without prior knowledge of the system dynamics. Motivated by a critical failure scenario in which a system can experience an abrupt change in its dynamics, we demonstrate that it is possible to follow a set of waypoints comprised of states analytically proven to be reachable despite not knowing the system dynamics. The proposed algorithm first applies small perturbations to locally learn the system dynamics around the current state, then computes the set of states that are provably reachable using the locally learned dynamics and their corresponding maximum growth-rate bounds, and finally synthesizes a control action that navigates the system to a guaranteed reachable state.

cs.RO↗

arXiv2025

Two-dimensional materials as a multiproperty sensing platform

Two-dimensional (2D) materials have disrupted materials science due to the development of van der Waals technology. It enables the stacking of ultrathin layers of materials characterized by vastly different electronic structures to create man-made heterostructures and devices with rationally tailored properties, circumventing limitations of matching crystal structures, lattice constants, and geometry of constituent materials and supporting substrates. 2D materials exhibit extraordinary mechanical flexibility, strong light-matter interactions driven by their excitonic response, single photon emission from atomic centers, stable ferromagnetism in sub-nm thin films, fractional quantum Hall effect in high-quality devices, and chemoselectivity at ultrahigh surface-to-volume ratio. Consequently, van der Waals heterostructures with atomically flat interfaces demonstrate an unprecedented degree of intertwined mechanical, chemical, optoelectronic, and magnetic properties. This constitutes a foundation for multiproperty sensing, based on complex intra- and intermaterial interactions, and a robust response to external stimuli originating from the environment. Here, we review recent progress in the development of sensing applications with 2D materials, highlighting the areas where van der Waals heterostructures offer the highest sensitivity, simultaneous responses to multiple distinct externalities due to their atomic thickness in conjunction with unique material combinations, and conceptually new sensing methodology.

cond-mat.mes-hall↗

arXiv2025

FiberKAN: Kolmogorov-Arnold Networks for Nonlinear Fiber Optics

Scientific discovery and dynamic characterization of the physical system play a critical role in understanding, learning, and modeling the physical phenomena and behaviors in various fields. Although theories and laws of many system dynamics have been derived from rigorous first principles, there are still a considerable number of complex dynamics that have not yet been discovered and characterized, which hinders the progress of science in corresponding fields. To address these challenges, artificial intelligence for science (AI4S) has emerged as a burgeoning research field. In this paper, a Kolmogorov-Arnold Network (KAN)-based AI4S framework named FiberKAN is proposed for scientific discovery and dynamic characterization of nonlinear fiber optics. Unlike the classic multi-layer perceptron (MLP) structure, the trainable and transparent activation functions in KAN make the network have stronger physical interpretability and nonlinear characterization abilities. Multiple KANs are established for fiber-optic system dynamics under various physical effects. Results show that KANs can well discover and characterize the explicit, implicit, and non-analytical solutions under different effects, and achieve better performance than MLPs with the equivalent scale of trainable parameters. Moreover, the effectiveness, computational cost, interactivity, noise resistance, transfer learning ability, and comparison between related algorithms in fiber-optic systems are also studied and analyzed. This work highlights the transformative potential of KAN, establishing it as a pioneering paradigm in AI4S that propels advancements in nonlinear fiber optics, and fosters groundbreaking innovations across a broad spectrum of scientific and engineering disciplines.

physics.optics↗

arXiv2025

Koopman Spectral Analysis and System Identification for Stochastic Dynamical Systems via Yosida Approximation of Generators

System identification and Koopman spectral analysis are crucial for uncovering physical laws and understanding the long-term behaviour of stochastic dynamical systems governed by stochastic differential equations (SDEs). In this work, we propose a novel method for estimating the Koopman generator of systems of SDEs, based on the theory of resolvent operators and the Yosida approximation. This enables both spectral analysis and accurate estimation and reconstruction of system parameters. The proposed approach relies on only mild assumptions about the system and effectively avoids the error amplification typically associated with direct numerical differentiation. It remains robust even under low sampling rates or with only a single observed trajectory, reliably extracting dominant spectral modes and dynamic features. We validate our method on two simple systems and compare it with existing techniques as benchmarks. The experimental results demonstrate the effectiveness and improved performance of our approach in system parameter estimation, spectral mode extraction, and overall robustness.

eess.SY↗

arXiv2025

Target Prediction Under Deceptive Switching Strategies via Outlier-Robust Filtering of Partially Observed Incomplete Trajectories

Motivated by a study on deception and counter-deception, this paper addresses the problem of identifying an agent's target as it seeks to reach one of two targets in a given environment. In practice, an agent may initially follow a strategy to aim at one target but decide to switch to another midway. Such a strategy can be deceptive when the counterpart only has access to imperfect observations, which include heavily corrupted sensor noise and possible outliers, making it difficult to visually identify the agent's true intent. To counter deception and identify the true target, we utilize prior knowledge of the agent's dynamics and the imprecisely observed partial trajectory of the agent's states to dynamically update the estimation of the posterior probability of whether a deceptive switch has taken place. However, existing methods in the literature have not achieved effective deception identification within a reasonable computation time. We propose a set of outlier-robust change detection methods to track relevant change-related statistics efficiently, enabling the detection of deceptive strategies in hidden nonlinear dynamics with reasonable computational effort. The performance of the proposed framework is examined for Weapon-Target Assignment (WTA) detection under deceptive strategies using random simulations in the kinematics model with external forcing.

stat.AP↗

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

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

Online Learning and Control Synthesis for Reachable Paths of Unknown Nonlinear Systems

In this paper, we present a novel method to drive a nonlinear system to a desired state, with limited a priori knowledge of its dynamic model: local dynamics at a single point and the bounds on the rate of change of these dynamics. This method synthesizes control actions by utilizing locally learned dynamics along a trajectory, based on data available up to that moment, and known proxy dynamics, which can generate an underapproximation of the unknown system's true reachable set. An important benefit to the contributions of this paper is the lack of knowledge needed to execute the presented control method. We establish sufficient conditions to ensure that a controlled trajectory reaches a small neighborhood of any provably reachable state within a short time horizon, with precision dependent on the tunable parameters of these conditions.

math.OC↗

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

Stochastic Control Barrier Functions with Bayesian Inference for Unknown Stochastic Differential Equations

Control barrier functions are widely used to synthesize safety-critical controls. However, the presence of Gaussian-type noise in dynamical systems can generate unbounded signals and potentially result in severe consequences. Although research has been conducted in the field of safety-critical control for stochastic systems, in many real-world scenarios, we do not have precise knowledge about the stochastic dynamics. In this paper, we delve into the safety-critical control for stochastic systems where both the drift and diffusion components are unknown. We employ Bayesian inference as a data-driven approach to approximate the system. To be more specific, we utilize Bayesian linear regression along with the central limit theorem to estimate the drift term, and employ Bayesian inference to approximate the diffusion term. Through simulations, we verify our findings by applying them to a nonlinear dynamical model and an adaptive cruise control model.

eess.SY↗