# TEMPEST -- Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments

arXiv: https://arxiv.org/abs/2105.12588 · HTML: https://mlsanity.com/paper/2105.12588/

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 May 2021.

## Built on by (most cited first, 13 of 13)

- [Online Shielding for Reinforcement Learning](https://mlsanity.com/paper/2212.01861/) (2022)
- [Verification-Guided Shielding for Deep Reinforcement Learning](https://mlsanity.com/paper/2406.06507/) (2024)
- [Shield Synthesis for LTL Modulo Theories](https://mlsanity.com/paper/2406.04184/) (2024)
- [Automata Learning meets Shielding](https://mlsanity.com/paper/2212.01838/) (2022)
- [Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games](https://mlsanity.com/paper/2405.03885/) (2024)
- [Conformal Safety Shielding for Imperfect-Perception Agents](https://mlsanity.com/paper/2506.17275/) (2025)
- [Analyzing Intentional Behavior in Autonomous Agents under Uncertainty](https://mlsanity.com/paper/2307.01532/) (2023)
- [Test Where Decisions Matter: Importance-driven Testing for Deep Reinforcement Learning](https://mlsanity.com/paper/2411.07700/) (2024)
- [Multi-Agent Verification and Control with Probabilistic Model Checking](https://mlsanity.com/paper/2308.02829/) (2023)
- [Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems](https://mlsanity.com/paper/2508.16345/) (2025)
- [Easy-to-Use Shielding for Reinforcement Learning](https://mlsanity.com/paper/2606.03804/) (2026)
- [Efficient Dynamic Shielding for Parametric Safety Specifications](https://mlsanity.com/paper/2505.22104/) (2025)
- [Explainably Safe Reinforcement Learning](https://mlsanity.com/paper/2606.04634/) (2026)

## Abstract (arXiv)

We present Tempest, a synthesis tool to automatically create correct-by-construction reactive systems and shields from qualitative or quantitative specifications in probabilistic environments. A shield is a special type of reactive system used for run-time enforcement; i.e., a shield enforces a given qualitative or quantitative specification of a running system while interfering with its operation as little as possible. Shields that enforce a qualitative or quantitative specification are called safety-shields or optimal-shields, respectively. Safety-shields can be implemented as pre-shields or as post-shields, optimal-shields are implemented as post-shields. Pre-shields are placed before the system and restrict the choices of the system. Post-shields are implemented after the system and are able to overwrite the system's output. Tempest is based on the probabilistic model checker Storm, adding model checking algorithms for stochastic games with safety and mean-payoff objectives. To the best of our knowledge, Tempest is the only synthesis tool able to solve 2-1/2-player games with mean-payoff objectives without restrictions on the state space. Furthermore, Tempest adds the functionality to synthesize safe and optimal strategies that implement reactive systems and shields