# Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Aug 2019.

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

- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [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)
- [Dynamic Shielding for Reinforcement Learning in Black-Box Environments](https://mlsanity.com/paper/2207.13446/) (2022)
- [Data-driven Design of Context-aware Monitors for Hazard Prediction in Artificial Pancreas Systems](https://mlsanity.com/paper/2104.02545/) (2021)
- [Ablation Study of How Run Time Assurance Impacts the Training and Performance of Reinforcement Learning Agents](https://mlsanity.com/paper/2207.04117/) (2022)
- [Efficient Dynamic Shielding for Parametric Safety Specifications](https://mlsanity.com/paper/2505.22104/) (2025)
- [Shielding for Higher-Order Safety](https://mlsanity.com/paper/2608.03662/) (2026)

## Abstract (arXiv)

Cyber-physical systems are often safety-critical in that violations of safety properties may lead to catastrophes. We propose a method to enforce the safety of systems with real-valued signals by synthesizing a runtime enforcer called the shield. Whenever the system violates a property, the shield, composed with the system, makes correction instantaneously to ensure that no erroneous output is generated by the combined system. While techniques for synthesizing Boolean shields are well understood, they do not handle real-valued signals ubiquitous in cyber-physical systems, meaning corrections may be either unrealizable or inefficient to compute in the real domain. We solve the realizability and efficiency problems by statically analyzing the compatibility of predicates defined over real-valued signals, and using the analysis result to constrain a two-player safety game used to synthesize the shield. We have implemented the method and demonstrated its effectiveness and efficiency on a variety of applications, including an automotive powertrain control system.