BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909602715533312 |
|---|---|
| author | Sidrane, Chelsea Tumova, Jana |
| author_facet | Sidrane, Chelsea Tumova, Jana |
| contents | Learning-enabled planning and control algorithms are increasingly popular, but they often lack rigorous guarantees of performance or safety. We introduce an algorithm for computing underapproximate backward reachable sets of nonlinear discrete time neural feedback loops. We then use the backward reachable sets to check goal-reaching properties. Our algorithm is based on overapproximating the system dynamics function to enable computation of underapproximate backward reachable sets through solutions of mixed-integer linear programs. We rigorously analyze the soundness of our algorithm and demonstrate it on a numerical example. Our work expands the class of properties that can be verified for learning-enabled systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_03643 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems Sidrane, Chelsea Tumova, Jana Artificial Intelligence Logic in Computer Science Systems and Control Learning-enabled planning and control algorithms are increasingly popular, but they often lack rigorous guarantees of performance or safety. We introduce an algorithm for computing underapproximate backward reachable sets of nonlinear discrete time neural feedback loops. We then use the backward reachable sets to check goal-reaching properties. Our algorithm is based on overapproximating the system dynamics function to enable computation of underapproximate backward reachable sets through solutions of mixed-integer linear programs. We rigorously analyze the soundness of our algorithm and demonstrate it on a numerical example. Our work expands the class of properties that can be verified for learning-enabled systems. |
| title | BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems |
| topic | Artificial Intelligence Logic in Computer Science Systems and Control |
| url | https://arxiv.org/abs/2505.03643 |