🤖 AI

Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems

This paper introduces Uppaal Coshy, an automatic tool that synthesizes compact safety shields for hybrid systems by approximating complex state-space partitions through simulations and employing the Caap algorithm to efficiently represent the resulting strategies as decision trees.

Original 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 2026-08-06

📖 7 min read🧠 Deep dive

CC BY 4.0

Original authors: Asger Horn Brorholt, Andreas Holck Høeg-Petersen, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikučionis, Christian Schilling, Andrzej Wąsowski

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to teach a robot how to play a game, like keeping a ball in the air or driving a car through a storm. You want the robot to be as good as possible, but you also need to make sure it never does something dangerous, like crashing into a wall or letting the ball drop. In the world of computer science, this is called "shield synthesis." Think of a shield not as a piece of metal, but as a strict safety coach that stands next to the robot. If the robot tries to make a move that could lead to disaster, the coach steps in and says, "Nope, not that one! Try this safe move instead." This is crucial for complex systems where the rules change constantly, like a bouncing ball that reacts to wind or a circuit that deals with electricity. The challenge is that these systems have infinite possibilities, making it incredibly hard to write down a perfect list of "safe" and "unsafe" moves for every single situation.

This is where the paper "Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems" comes in. The researchers, a team from Denmark, have built a new tool called Uppaal Coshy that acts like a super-smart safety coach for these tricky, mixed-up systems (which they call "hybrid systems" because they mix smooth, continuous changes like speed with sudden, digital jumps like turning a switch on or off). Their big idea is to first divide the entire universe of possible situations into a giant grid of tiny boxes. They then run thousands of simulations to figure out which boxes are safe and which are dangerous, creating a massive map of allowed moves. However, this map can get so huge that it's impossible to store or use. To solve this, they invented a clever algorithm called "Caap" (which sounds like a friendly robot name) that takes this giant, messy map and squashes it down into a neat, compact decision tree—like turning a 100-page instruction manual into a simple flowchart. They tested this on a bouncing ball model and found that their method could shrink the safety rules by thousands of times without losing any safety, making it possible to put these safety coaches on real devices.

The Story of the Bouncing Ball and the Safety Coach

Let's dive into the heart of the story with a character we all know: a bouncing ball. Imagine a ball that is bouncing up and down. A human player can hit it to keep it going, but if they hit it too hard or at the wrong time, the ball might fly off into the sky or stop bouncing entirely. The goal is to keep the ball bouncing forever without it ever stopping or flying away.

In the old days, figuring out exactly when to hit the ball to keep it safe would be a nightmare. The ball's position and speed change smoothly and continuously, meaning there are infinite places it could be at any second. The researchers used a tool called Uppaal Coshy to solve this. They treated the ball's world like a giant checkerboard. They chopped up the space where the ball could be into millions of tiny, rectangular boxes. For each box, the tool asked a simple question: "If the ball is in this box, what moves are safe?"

To answer this, the tool didn't just guess; it played the game over and over again. It picked a spot inside a box, simulated the ball bouncing, and watched where it landed. If the ball landed in a "safe" box, that move was good. If it landed in a "danger" box (like the one where the ball stops), that move was banned. Because the ball's behavior can be a little random (maybe the floor is bumpy, or the hit isn't perfect), the tool ran these simulations many times to be sure. They even had to deal with the fact that the ball might bounce so high it leaves the "board" entirely. The tool handled this by creating a special "out-of-bounds" zone and deciding whether leaving the board was safe or not based on what happened in the simulations.

The Problem of the Giant Map

Here is where the story hits a snag. Because the grid was so fine (to be very precise), the tool ended up with a massive list of rules. For their bouncing ball example, the initial safety map had over 1.4 million tiny boxes, each with its own rule about what to do. Storing a list that big is like trying to carry a library in your backpack; it's too heavy for a real robot to use.

The researchers noticed something interesting: many of the boxes right next to each other had the exact same rules. If the ball is in a box where it's safe to hit, the ball in the box right next to it is probably safe to hit too. So, instead of keeping millions of tiny rules, why not group them together?

Enter Caap: The Magic Compressor

This is where their new algorithm, Caap, steps in. Think of Caap as a magical editor that looks at the giant, messy map and says, "Hey, these 500 boxes all say 'Hit the ball.' Let's merge them into one big zone." It does this by looking for patterns and merging neighboring boxes into larger, rectangular regions, as long as the rules stay the same.

The result is a decision tree. Imagine a flowchart: "Is the ball high? Yes? Is it moving fast? No? Then hit it." This tree is much smaller and easier to read than the original million-box map. In their tests, Caap managed to shrink the bouncing ball's safety rules from 1,430,000 tiny cells down to just 2,972 regions. That's a huge reduction! It's like turning a 1,000-page novel into a 20-page comic book that tells the exact same story.

Does It Actually Work?

The team didn't just make the map smaller; they made sure it still worked. They tested their new, compact shield on the bouncing ball. They ran 10,000 simulations where the ball was controlled by this new, compressed safety coach. The result? In none of those 10,000 runs did the ball ever stop bouncing or fly away. The safety was preserved perfectly, even though the rules were now tiny enough to fit on a postcard.

They also showed that this safety coach could be used to teach the robot to be better. First, they let the robot learn how to hit the ball efficiently (using as little energy as possible) while the shield stood guard to stop it from making dangerous mistakes. The robot learned to keep the ball in the air with very few hits, proving that you can have both safety and efficiency at the same time.

Why This Matters

This paper isn't just about bouncing balls. The same math applies to real-world things like electric circuits (called boost converters) that need to keep voltage steady, or water tanks that need to avoid overflowing. The researchers tested their tool on these models too, and in every case, the Caap algorithm successfully shrunk the safety rules by a massive amount—sometimes reducing millions of rules down to just a few dozen—while keeping the system safe.

The beauty of Uppaal Coshy is that it's fully automatic. You don't need to be a math genius to use it; you just describe your system, and the tool figures out the safety rules, compresses them, and gives you a compact shield ready to use. It's a big step forward for making sure that the smart robots and automated systems of the future are not only smart but also safe, reliable, and small enough to run on the devices we use every day.

Technical Summary: Uppaal Coshy – Automatic Synthesis of Compact Shields for Hybrid Systems

1. Problem Statement

The paper addresses the challenge of synthesizing safety strategies (shields) for Markov Decision Processes (MDPs) over continuous state spaces with complex hybrid dynamics. Unlike discrete state spaces where shield synthesis is well-established, hybrid systems present algorithmic difficulties, particularly regarding reachability analysis for non-linear dynamics and the management of infinite state spaces.

A primary practical bottleneck identified is the scalability and storage of synthesized shields. Traditional partition-based approaches store allowed actions for every individual cell in a grid, resulting in massive data structures that are inefficient for storage and deployment, especially on embedded devices. Furthermore, determining safe cells and transitions in general hybrid systems often involves undecidable reachability problems.

2. Methodology

The authors present Uppaal Coshy, a tool fully integrated into the Uppaal modeling environment. The methodology combines a partition-based synthesis algorithm with simulation-based approximations and a novel compression technique.

2.1 Partition-Based Shield Synthesis

The core algorithm abstracts the continuous state space $S \subseteq \mathbb{R}^k$ into a finite set of disjoint rectangular cells using a regular grid defined by a granularity vector $\gamma$ and an offset $\omega$ .

Safety Game Formulation: The synthesis is framed as a two-player safety game. The goal is to compute the maximal set of "safe cells" ( $C_\phi$ ) from which the system can remain within a safety property $\phi$ indefinitely.
Approximation via Simulation: Since exact reachability is often undecidable for general hybrid systems, the tool employs a simulation-based approach:
- Initial Safe Cells ( $C^0_\phi$ ): Instead of symbolic reasoning, the tool systematically samples points within each cell. A cell is deemed initially safe only if all sampled points satisfy the safety specification.
- Transition Relation: To determine if a transition exists between cells ( $C \xrightarrow{a} C'$ ), the tool simulates the system dynamics from sampled states in $C$ using action $a$ . If the simulation reaches a state where the controller must make a new choice, the corresponding target cell is added to the transition relation.
- Stochasticity: Unlike prior work that required manual crafting of sampling for stochastic dimensions, Uppaal Coshy allows the simulator to sample directly from stochastic distributions, supporting general distributions with unbounded support.

2.2 Handling Practical Challenges

Unbounded State Spaces: The tool handles systems where state bounds are not immediately clear (e.g., a bouncing ball) by introducing a dummy "out-of-bounds" cell ( $C_{out}$ ). Users can configure whether leaving bounds is safe, unsafe, or determined via sampling.
Variable Omission: To reduce dimensionality, users can omit variables (e.g., cost counters or clocks) from the grid partitioning. These variables are fixed to their initial values during synthesis, provided they do not influence the safety logic.

2.3 Compact Representation: The Caap Algorithm

To address the storage inefficiency of grid-based shields, the authors introduce Caap (Coarsify Axis-Aligned Partitionings).

Goal: Transform a fine-grained, axis-aligned grid-based shield into a compact, equivalent decision tree.
Mechanism: The algorithm iteratively merges neighboring cells that share the same set of allowed actions into larger rectangular "regions."
Constraints: Merges are subject to three expansion rules to ensure the resulting partitioning remains valid:
1. All cells in the new region must have the same action set.
2. The new region must not intersect with existing regions in the new partitioning.
3. The expansion must not cut any original region into non-rectangular fragments.
Result: This yields a decision tree where internal nodes represent axis-aligned predicates ( $s_i < c$ ) and leaves represent sets of allowed actions, significantly reducing the representation size.

3. Key Contributions

Uppaal Coshy Tool: A fully automatic tool for shield synthesis in Uppaal, supporting expressive formalisms including stochastic hybrid automata and external C library calls. It integrates with Uppaal Stratego to enable reinforcement learning under a synthesized shield.
Caap Algorithm: A novel algorithm for compressing grid-based shields into decision trees, preserving functionality while drastically reducing size.
Simulation-Based Approximation: A practical implementation strategy that bypasses undecidable reachability problems by using systematic sampling and simulation, supporting non-periodic control and general stochastic distributions.

4. Results and Evaluation

The authors evaluated the tool on four models: a bouncing ball, a boost converter, a random walk, and a water tank.

Synthesis and Reduction: Table 2 in the paper demonstrates significant reductions in shield size. For the bouncing ball model, the shield was reduced from 1,430,000 cells to 2,972 regions (a reduction factor of ~480x) in 53 seconds. The boost converter saw a reduction from 136,800 to 571 regions.
Safety Verification: All synthesized shields were statistically evaluated with 99% confidence intervals over 10,000 runs. No unsafe runs were observed, confirming the shields maintained safety properties (e.g., preventing the ball from stopping or the voltage from exceeding bounds).
Workflow Demonstration: The bouncing ball case study (Section 5.1) illustrates a complete workflow: synthesizing a basic "efficient" strategy (which fails safety), generating a shield, compressing it via Caap, and finally using Uppaal Stratego to learn a near-optimal strategy under the compact shield. The resulting strategy was both safe and efficient.

5. Significance and Claims

The paper positions Uppaal Coshy as a bridge between theoretical shield synthesis and practical application in complex hybrid systems.

Expressiveness: The tool claims to handle a richer class of models than existing tools (like Tempest or Uppaal Tiga), specifically supporting stochastic hybrid systems with non-periodic control and external code integration.
Deployability: By introducing the Caap algorithm, the authors claim to solve the critical problem of shield size, making the deployment of synthesized strategies on resource-constrained embedded devices feasible.
Integration: The seamless integration with Uppaal Stratego allows for a workflow where safety is guaranteed by the shield, while performance is optimized via reinforcement learning, a capability the authors highlight as a distinct benefit over prior work.

The authors remain modest regarding the approximation nature of their approach, noting that the simulation-based under-approximation relies on the number of samples ( $n$ ) and re-sampling runs ( $m$ ) to approach the true solution, and that the Caap algorithm is currently a standalone tool that they propose integrating directly into the Uppaal user interface in future work.