Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916912121774080 |
|---|---|
| author | Brorholt, Asger Horn Høeg-Petersen, Andreas Holck Jensen, Peter Gjøl Larsen, Kim Guldstrand Mikučionis, Marius Schilling, Christian Wąsowski, Andrzej |
| author_facet | Brorholt, Asger Horn Høeg-Petersen, Andreas Holck Jensen, Peter Gjøl Larsen, Kim Guldstrand Mikučionis, Marius Schilling, Christian Wąsowski, Andrzej |
| contents | We present Uppaal Coshy, a tool for automatic synthesis of a safety strategy -- or shield -- for Markov decision processes over continuous state spaces and complex hybrid dynamics. The general methodology is to partition the state space and then solve a two-player safety game, which entails a number of algorithmically hard problems such as reachability for hybrid systems. The general philosophy of Uppaal Coshy is to approximate hard-to-obtain solutions using simulations. Our implementation is fully automatic and supports the expressive formalism of Uppaal models, which encompass stochastic hybrid automata. The precision of our partition-based approach benefits from using finer grids, which however are not efficient to store. We include an algorithm called Caap to efficiently compute a compact representation of a shield in the form of a decision tree, which yields significant reductions. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_16345 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems Brorholt, Asger Horn Høeg-Petersen, Andreas Holck Jensen, Peter Gjøl Larsen, Kim Guldstrand Mikučionis, Marius Schilling, Christian Wąsowski, Andrzej Logic in Computer Science Artificial Intelligence Machine Learning We present Uppaal Coshy, a tool for automatic synthesis of a safety strategy -- or shield -- for Markov decision processes over continuous state spaces and complex hybrid dynamics. The general methodology is to partition the state space and then solve a two-player safety game, which entails a number of algorithmically hard problems such as reachability for hybrid systems. The general philosophy of Uppaal Coshy is to approximate hard-to-obtain solutions using simulations. Our implementation is fully automatic and supports the expressive formalism of Uppaal models, which encompass stochastic hybrid automata. The precision of our partition-based approach benefits from using finer grids, which however are not efficient to store. We include an algorithm called Caap to efficiently compute a compact representation of a shield in the form of a decision tree, which yields significant reductions. |
| title | Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems |
| topic | Logic in Computer Science Artificial Intelligence Machine Learning |
| url | https://arxiv.org/abs/2508.16345 |