Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909980405268480 |
|---|---|
| author | Xue, Bai |
| author_facet | Xue, Bai |
| contents | This paper investigates necessary and sufficient barrier-like conditions for infinite-horizon safety and reach-avoid verification of stochastic discrete-time systems, derived via a relaxation of the Bellman equations. Unlike prior approaches that primarily focus on sufficient conditions, our work rigorously establishes both necessity and sufficiency for infinite-horizon properties. Safety verification concerns certifying that, starting from a given initial state, the system remains within a safe set at all future time steps with probability at least equal to a specified threshold. For this purpose, we formulate a necessary and sufficient barrier-like condition that captures this infinite-time safety property. In contrast, reach-avoid verification generalizes safety verification by also incorporating reachability. Specifically, it aims to ensure that the probability of the system, starting from a given initial state, eventually reaching a target set while remaining within the safe set until the first hit of the target is no less than a prescribed bound. Under suitable assumptions, we establish two necessary and sufficient barrier-like conditions for this reach-avoid specification. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_15572 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems Xue, Bai Systems and Control This paper investigates necessary and sufficient barrier-like conditions for infinite-horizon safety and reach-avoid verification of stochastic discrete-time systems, derived via a relaxation of the Bellman equations. Unlike prior approaches that primarily focus on sufficient conditions, our work rigorously establishes both necessity and sufficiency for infinite-horizon properties. Safety verification concerns certifying that, starting from a given initial state, the system remains within a safe set at all future time steps with probability at least equal to a specified threshold. For this purpose, we formulate a necessary and sufficient barrier-like condition that captures this infinite-time safety property. In contrast, reach-avoid verification generalizes safety verification by also incorporating reachability. Specifically, it aims to ensure that the probability of the system, starting from a given initial state, eventually reaching a target set while remaining within the safe set until the first hit of the target is no less than a prescribed bound. Under suitable assumptions, we establish two necessary and sufficient barrier-like conditions for this reach-avoid specification. |
| title | Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems |
| topic | Systems and Control |
| url | https://arxiv.org/abs/2408.15572 |