# Shield Synthesis for LTL Modulo Theories

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

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- Builds on 34 of its 95 references that are in the map.
- First posted on arXiv 6 Jun 2024.

## Builds on (most cited first, 30 of 34)

- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Deep Reinforcement Learning with Double Q-learning](https://mlsanity.com/paper/1509.06461/) (2015)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [Shield Synthesis: Runtime Enforcement for Reactive Systems](https://mlsanity.com/paper/1501.02573/) (2015)
- [Fastened CROWN: Tightened Neural Network Robustness Certificates](https://mlsanity.com/paper/1912.00574/) (2019)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Safe Reinforcement Learning using Formal Verification for Tissue Retraction in Autonomous Robotic-Assisted Surgery](https://mlsanity.com/paper/2109.02323/) (2021)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [Extending the OpenAI Gym for robotics: a toolkit for reinforcement learning using ROS and Gazebo](https://mlsanity.com/paper/1608.05742/) (2016)
- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [TEMPEST -- Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments](https://mlsanity.com/paper/2105.12588/) (2021)
- [veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System](https://mlsanity.com/paper/2212.03287/) (2022)
- [Constrained Reinforcement Learning for Robotics via Scenario-Based Programming](https://mlsanity.com/paper/2206.09603/) (2022)
- [Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems](https://mlsanity.com/paper/1908.05402/) (2019)
- [Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts](https://mlsanity.com/paper/1709.04986/) (2017)
- [Decidable Fragments of LTLf Modulo Theories (Extended Version)](https://mlsanity.com/paper/2307.16840/) (2023)
- [Choice Logics and Their Computational Properties](https://mlsanity.com/paper/2106.05052/) (2021)
- [Reactive Synthesis Modulo Theories Using Abstraction Refinement](https://mlsanity.com/paper/2108.00090/) (2021)
- [AbsSynthe: abstract synthesis from succinct safety specifications](https://mlsanity.com/paper/1407.5961/) (2014)

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

- [Verification-Guided Shielding for Deep Reinforcement Learning](https://mlsanity.com/paper/2406.06507/) (2024)
- [Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretation](https://mlsanity.com/paper/2408.03915/) (2024)
- [Safe and Reliable Training of Learning-Based Aerospace Controllers](https://mlsanity.com/paper/2407.07088/) (2024)
- [Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis](https://mlsanity.com/paper/2407.09348/) (2024)
- [Shields to Guarantee Probabilistic Safety in MDPs](https://mlsanity.com/paper/2605.10888/) (2026)
- [Easy-to-Use Shielding for Reinforcement Learning](https://mlsanity.com/paper/2606.03804/) (2026)
- [Research Vision: Multi-Agent Path Planning for Cops And Robbers Via Reactive Synthesis](https://mlsanity.com/paper/2503.11475/) (2025)
- [Efficient Dynamic Shielding for Parametric Safety Specifications](https://mlsanity.com/paper/2505.22104/) (2025)
- [Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version)](https://mlsanity.com/paper/2602.06227/) (2026)
- [Is Your Agent Playing Dead? Deployed LLM Agents Exhibit Constraint-Evasive Fabrication and Thanatosis](https://mlsanity.com/paper/2606.14831/) (2026)
- [Cycle-Consistent Neural Explanation of Formal Verification Certificates](https://mlsanity.com/paper/2606.24414/) (2026)
- [Shielding for Higher-Order Safety](https://mlsanity.com/paper/2608.03662/) (2026)

## Abstract (arXiv)

In recent years, Machine Learning (ML) models have achieved remarkable success in various domains. However, these models also tend to demonstrate unsafe behaviors, precluding their deployment in safety-critical systems. To cope with this issue, ample research focuses on developing methods that guarantee the safe behaviour of a given ML model. A prominent example is shielding which incorporates an external component (a ``shield'') that blocks unwanted behavior. Despite significant progress, shielding suffers from a main setback: it is currently geared towards properties encoded solely in propositional logics (e.g., LTL) and is unsuitable for richer logics. This, in turn, limits the widespread applicability of shielding in many real-world systems. In this work, we address this gap, and extend shielding to LTL modulo theories, by building upon recent advances in reactive synthesis modulo theories. This allowed us to develop a novel approach for generating shields conforming to complex safety specifications in these more expressive, logics. We evaluated our shields and demonstrate their ability to handle rich data with temporal dynamics. To the best of our knowledge, this is the first approach for synthesizing shields for such expressivity.