Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems

TL;DR

Uppaal Coshy is an automated tool that synthesizes compact safety shields for complex hybrid systems by approximating solutions through simulations and decision tree representations, improving efficiency.

Contribution

The paper introduces Uppaal Coshy, a novel automated method for synthesizing compact safety shields for hybrid systems using simulation-based approximations and decision trees.

Findings

Efficient synthesis of safety shields for hybrid systems.

Use of decision trees for compact shield representation.

Supports complex stochastic hybrid automata models.

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.