Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems
This work addresses safety assurance for hybrid systems, which is critical in domains like robotics and control, but it appears incremental as it builds on existing partition-based and game-solving methods with a focus on efficiency.
The authors tackled the problem of automatically synthesizing safety strategies (shields) for hybrid systems with continuous state spaces by partitioning the state space and solving safety games, resulting in a tool called Uppaal Coshy that uses simulations and a compact decision tree representation to achieve significant reductions in storage.
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.