Formally Verified Neural Lyapunov Function for Incremental Input-to-State Stability of Unknown Systems
This work presents an approach to synthesize a Lyapunov-like function to ensure incrementally input-to-state stability ($\delta$-ISS) property for an unknown discrete-time system. To deal with challenges posed by unknown system dynamics, we parameterize the Lyapunov-like function as a neural network, which we train using the data samples collected from the unknown system along with appropriately designed loss functions. We propose a validity condition to test the obtained function and incorporate it into the training framework to ensure provable correctness at the end of the training. Finally, the usefulness of the proposed technique is proved using two case studies: a scalar non-linear dynamical system and a permanent magnet DC motor.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Formally Verified Neural Network Controllers for Incremental Input-to-State Stability of Unknown Discrete-Time Systems
This work aims to synthesize a controller that ensures that an unknown discrete-time system is incrementally input-to-state stable ($\delta$-ISS). In this work, we introduce the notion of $\delta$-ISS control Lyapunov fu…
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…
A Test-Function Approach to Incremental Stability
This paper presents a novel framework for analyzing Incremental-Input-to-State Stability ($δ$ISS) based on the idea of using rewards as "test functions." Whereas control theory traditionally deals with Lyapunov functions…
Reinforcement LearningRobust stability of moving horizon estimation for continuous-time systems
We consider a moving horizon estimation (MHE) scheme involving a discounted least squares objective for general nonlinear continuous-time systems. Provided that the system is detectable (incrementally integral input/outp…
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
Deep reinforcement learning (DRL) is a powerful machine learning paradigm for generating agents that control autonomous systems. However, the ``black box'' nature of DRL agents limits their deployment in real-world safet…
Deep Reinforcement Learningreinforcement-learningReinforcement Learning