Complete Robust Hybrid Systems Reachability
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915818714955776 |
|---|---|
| author | Wafa, Noah Abou El Platzer, André |
| author_facet | Wafa, Noah Abou El Platzer, André |
| contents | This paper introduces robust differential dynamic logic (a fragment of differential dynamic logic) to specify and reason about robust hybrid systems. Practically meaningful syntactic restrictions naturally ensure that definable properties are topologically open and thus by construction robust with respect to infinitesimal perturbations, without explicit quantitative margins of error in the syntax or in proofs.
The main result is a proof of absolute completeness of robust differential dynamic logic for reachability properties of general hybrid systems. This is the first absolute completeness proof for hybrid systems with exact semantics. The proof is constructive, self-contained, and demonstrates how robustly correct hybrid systems reachability specifications can be automatically verified through proof. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_22853 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Complete Robust Hybrid Systems Reachability Wafa, Noah Abou El Platzer, André Logic in Computer Science 03B70 (Primary) 68N30 (Secondary) F.3.1; I.2.3; F.4.1 This paper introduces robust differential dynamic logic (a fragment of differential dynamic logic) to specify and reason about robust hybrid systems. Practically meaningful syntactic restrictions naturally ensure that definable properties are topologically open and thus by construction robust with respect to infinitesimal perturbations, without explicit quantitative margins of error in the syntax or in proofs. The main result is a proof of absolute completeness of robust differential dynamic logic for reachability properties of general hybrid systems. This is the first absolute completeness proof for hybrid systems with exact semantics. The proof is constructive, self-contained, and demonstrates how robustly correct hybrid systems reachability specifications can be automatically verified through proof. |
| title | Complete Robust Hybrid Systems Reachability |
| topic | Logic in Computer Science 03B70 (Primary) 68N30 (Secondary) F.3.1; I.2.3; F.4.1 |
| url | https://arxiv.org/abs/2602.22853 |