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 function ($\delta$-ISS-CLF), which, in conjunction with the controller, ensures that the closed-loop system is incrementally ISS. To address the unknown dynamics of the system, we parameterize the controller as well as the $\delta$-ISS-CLF as neural networks and learn them by utilizing the sampled data from the state space of the unknown system. To formally verify the obtained $\delta$-ISS-CLF, we develop a validity condition and incorporate the condition into the training framework to ensure a provable correctness guarantee at the end of the training process. Finally, the usefulness of the proposed approach is proved using multiple case studies - the first one is a scalar system with a non-affine non-polynomial structure, the second example is a one-link manipulator system, the third system is a nonlinear Moore-Grietzer model of the jet engine and the final one is a rotating rigid spacecraft model.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Verified Safe Reinforcement Learning for Neural Network Dynamic Models
Learning reliably safe autonomous control is one of the core problems in trustworthy autonomy. However, training a controller that can be formally verified to be safe remains a major challenge. We introduce a novel appro…
reinforcement-learningReinforcement LearningSafe Reinforcement LearningRuntime Safety Assurance Using Reinforcement Learning
The airworthiness and safety of a non-pedigreed autopilot must be verified, but the cost to formally do so can be prohibitive. We can bypass formal verification of non-pedigreed components by incorporating Runtime Safety…
reinforcement-learningReinforcement LearningReinforcement Learning (RL)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…
Certified Learning of Incremental ISS Controllers for Unknown Nonlinear Polynomial Dynamics
Incremental input-to-state stability (delta-ISS) offers a robust framework to ensure that small input variations result in proportionally minor deviations in the state of a nonlinear system. This property is essential in…
LEMMASandboxing (AI-based) Unverified Controllers in Stochastic Games: An Abstraction-based Approach with Safe-visor Architecture
In this paper, we propose a construction scheme for a Safe-visor architecture for sandboxing unverified controllers, e.g., artificial intelligence-based (a.k.a. AI-based) controllers, in two-players non-cooperative stoch…