Fully-Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2022
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909116122791936 |
|---|---|
| author | Wetzlinger, Mark Kochdumper, Niklas Bak, Stanley Althoff, Matthias |
| author_facet | Wetzlinger, Mark Kochdumper, Niklas Bak, Stanley Althoff, Matthias |
| contents | Reachability analysis is a formal method to guarantee safety of dynamical systems under the influence of uncertainties. A substantial bottleneck of all reachability algorithms is the necessity to adequately tune specific algorithm parameters, such as the time step size, which requires expert knowledge. In this work, we solve this issue with a fully automated reachability algorithm that tunes all algorithm parameters internally such that the reachable set enclosure respects a user-defined approximation error bound in terms of the Hausdorff distance to the exact reachable set. Moreover, this bound can be used to extract an inner-approximation of the reachable set from the outer-approximation using the Minkowski difference. Finally, we propose a novel verification algorithm that automatically refines the accuracy of the outer-approximation and inner-approximation until specifications given by time-varying safe and unsafe sets can be verified or falsified. The numerical evaluation demonstrates that our verification algorithm successfully verifies or falsifies benchmarks from different domains without requiring manual tuning. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2209_09321 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Fully-Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets Wetzlinger, Mark Kochdumper, Niklas Bak, Stanley Althoff, Matthias Numerical Analysis Systems and Control 65L70 G.1.7 Reachability analysis is a formal method to guarantee safety of dynamical systems under the influence of uncertainties. A substantial bottleneck of all reachability algorithms is the necessity to adequately tune specific algorithm parameters, such as the time step size, which requires expert knowledge. In this work, we solve this issue with a fully automated reachability algorithm that tunes all algorithm parameters internally such that the reachable set enclosure respects a user-defined approximation error bound in terms of the Hausdorff distance to the exact reachable set. Moreover, this bound can be used to extract an inner-approximation of the reachable set from the outer-approximation using the Minkowski difference. Finally, we propose a novel verification algorithm that automatically refines the accuracy of the outer-approximation and inner-approximation until specifications given by time-varying safe and unsafe sets can be verified or falsified. The numerical evaluation demonstrates that our verification algorithm successfully verifies or falsifies benchmarks from different domains without requiring manual tuning. |
| title | Fully-Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets |
| topic | Numerical Analysis Systems and Control 65L70 G.1.7 |
| url | https://arxiv.org/abs/2209.09321 |