{"ID":2879432,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2508.16345","arxiv_id":"2508.16345","title":"Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems","abstract":"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.","short_abstract":"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...","url_abs":"https://arxiv.org/abs/2508.16345","url_pdf":"https://arxiv.org/pdf/2508.16345v1","authors":"[\"Asger Horn Brorholt\",\"Andreas Holck Høeg-Petersen\",\"Peter Gjøl Jensen\",\"Kim Guldstrand Larsen\",\"Marius Mikučionis\",\"Christian Schilling\",\"Andrzej Wąsowski\"]","published":"2025-08-22T12:39:40Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.AI\",\"cs.LG\"]","methods":"[]","has_code":false}