A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems
Forward reachability analysis is the predominant approach for verifying reach-avoid properties in neural feedback systems (dynamical systems controlled by neural networks). This dominance stems from the limited scalability of existing backward reachability methods. In this work, we introduce new algorithms that compute both over- and under-approximations of backward reachable sets for such systems. We further integrate these backward algorithms with established forward analysis techniques to yield a unified verification framework for neural feedback systems.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
The FABRIC Strategy for Verifying Neural Feedback Systems
Forward reachability analysis is a dominant approach for verifying reach-avoid specifications in neural feedback systems, i.e., dynamical systems controlled by neural networks, and a number of directions have been propos…
Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
We consider the verification of neural network policies for discrete-time stochastic systems with respect to reach-avoid specifications. We use a learner-verifier procedure that learns a certificate for the specification…
Value Functions for Temporal Logic: Optimal Policies and Safety Filters
While Bellman equations for basic reach, avoid, and reach-avoid problems are well studied, the relationship between value optimality and policy optimality becomes subtle in the undiscounted infinite-horizon setting, part…
Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties
Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty. Often they are viewed as state transformers with planning objectives defined with respect to paths over MDP state…
Synthesis-guided Adversarial Scenario Generation for Gray-box Feedback Control Systems with Sensing Imperfections
In this paper, we study feedback dynamical systems with memoryless controllers under imperfect information. We develop an algorithm that searches for "adversarial scenarios", which can be thought of as the strategy for t…