2025/08/22 by Asger Horn Brorholt, Andreas Holck Høeg-Petersen, Brorholt, Asger Horn +11 · 1 citation
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Machine Learning (cs.LG) #cs.AI #cs.LG #cs.LO
paper · pdf · doi:10.48550/arxiv.2508.16345
published as RP 2025 · 12 pages and 6 figures. Additional abstract of 4 pages and 4 figures. Extended version with supplementary material for an article to appear in the 2025 International Conference on Reachability Problems (RP)
arxiv created 2025/08/22 · arxiv updated 2026/08/06
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.