Computing Sound Lower and Upper Bounds on Hamilton-Jacobi Reach-Avoid Value Functions
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911549383245824 |
|---|---|
| author | Tabbara, Ihab Badr, Eliya Sibai, Hussein |
| author_facet | Tabbara, Ihab Badr, Eliya Sibai, Hussein |
| contents | Hamilton-Jacobi (HJ) reachability analysis is a fundamental tool for the safety verification and control synthesis of nonlinear control systems. Classical HJ reachability analysis methods compute value functions over grids which discretize the continuous state space. Such approaches do not account for discretization errors and thus do not guarantee that the sets represented by the computed value functions over-approximate the backward reachable sets (BRS) when given avoid specifications or under-approximate the reach-avoid sets (RAS) when given reach-avoid specifications. We address this issue by presenting an algorithm for computing sound upper and lower bounds on the HJ value functions that guarantee the sound over-approximation of BRS and under-approximation of RAS. Additionally, we develop a refinement algorithm that splits the grid cells which could not be classified as within or outside the BRS or RAS given the computed bounds to obtain corresponding tighter bounds. We validate the effectiveness of our algorithm in two case studies. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_15238 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Computing Sound Lower and Upper Bounds on Hamilton-Jacobi Reach-Avoid Value Functions Tabbara, Ihab Badr, Eliya Sibai, Hussein Systems and Control Formal Languages and Automata Theory Symbolic Computation Hamilton-Jacobi (HJ) reachability analysis is a fundamental tool for the safety verification and control synthesis of nonlinear control systems. Classical HJ reachability analysis methods compute value functions over grids which discretize the continuous state space. Such approaches do not account for discretization errors and thus do not guarantee that the sets represented by the computed value functions over-approximate the backward reachable sets (BRS) when given avoid specifications or under-approximate the reach-avoid sets (RAS) when given reach-avoid specifications. We address this issue by presenting an algorithm for computing sound upper and lower bounds on the HJ value functions that guarantee the sound over-approximation of BRS and under-approximation of RAS. Additionally, we develop a refinement algorithm that splits the grid cells which could not be classified as within or outside the BRS or RAS given the computed bounds to obtain corresponding tighter bounds. We validate the effectiveness of our algorithm in two case studies. |
| title | Computing Sound Lower and Upper Bounds on Hamilton-Jacobi Reach-Avoid Value Functions |
| topic | Systems and Control Formal Languages and Automata Theory Symbolic Computation |
| url | https://arxiv.org/abs/2511.15238 |