mlsanityData to 7 Oct 2026

Shield Synthesis for LTL Modulo Theories

arXiv 2406.04184 ↗First posted 6 Jun 2024cs.LO cs.AI cs.LGcited by 12

Not on the map. Why?

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.

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

Builds on

34 of 95 references.

References · 34

  1. 2017Proximal Policy Optimization Algorithmscited by 14,441
  2. 2014Explaining and Harnessing Adversarial Examplescited by 7,287
  3. 2015Deep Reinforcement Learning with Double Q-learningcited by 1,704
  4. 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 739
  5. 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 439
  6. 2016Safety Verification of Deep Neural Networkscited by 262
  7. 2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 224
  8. 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
  9. 2020NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systemscited by 128
  10. 2024Marabou 2.0: A Versatile Formal Analyzer of Neural Networkscited by 81
  11. 2020Verification of Deep Convolutional Neural Networks Using ImageStarscited by 75
  12. 2020An SMT-Based Approach for Verifying Binarized Neural Networkscited by 47
22 more
  1. 2015Shield Synthesis: Runtime Enforcement for Reactive Systemscited by 41
  2. 2019Fastened CROWN: Tightened Neural Network Robustness Certificatescited by 39
  3. 2021Neural Network Robustness as a Verification Property: A Principled Case Studycited by 35
  4. 2021Towards Scalable Verification of Deep Reinforcement Learningcited by 33
  5. 2022Verifying Learning-Based Robotic Navigation Systemscited by 33
  6. 2023Formally Explaining Neural Networks within Reactive Systemscited by 24
  7. 2021Safe Reinforcement Learning using Formal Verification for Tissue Retraction in Autonomous Robotic-Assisted Surgerycited by 22
  8. 2016Extending the OpenAI Gym for robotics: a toolkit for reinforcement learning using ROS and Gazebocited by 18
  9. 2024Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificatescited by 15
  10. 2021TEMPEST -- Synthesis Tool for Reactive Systems and Shields in Probabilistic Environmentscited by 13
  11. 2022veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection Systemcited by 12
  12. 2022Constrained Reinforcement Learning for Robotics via Scenario-Based Programmingcited by 11
  13. 2019Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systemscited by 8
  14. 2017Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contractscited by 6
  15. 2023Decidable Fragments of LTLf Modulo Theories (Extended Version)cited by 5
  16. 2021Choice Logics and Their Computational Propertiescited by 3
  17. 2021Reactive Synthesis Modulo Theories Using Abstraction Refinementcited by 3
  18. 2014AbsSynthe: abstract synthesis from succinct safety specificationscited by 2
  19. 2015Towards Realizability Checking of Contracts using Theoriescited by 2
  20. 2016Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logiccited by 2
  21. 2016Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizabilitycited by 2
  22. 2017On Optimization Modulo Theories, MaxSMT and Sorting Networkscited by 2

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 4; 2025: 2; 2026: 6.

12 papers.

  1. 2024Verification-Guided Shielding for Deep Reinforcement Learningcited by 13
  2. 2024Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretationcited by 11
  3. 2024Safe and Reliable Training of Learning-Based Aerospace Controllerscited by 4
  4. 2024Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesiscited by 2
  5. 2026Shields to Guarantee Probabilistic Safety in MDPscited by 2
  6. 2026Easy-to-Use Shielding for Reinforcement Learningcited by 1
  7. 2025Research Vision: Multi-Agent Path Planning for Cops And Robbers Via Reactive Synthesiscited by 0
  8. 2025Efficient Dynamic Shielding for Parametric Safety Specificationscited by 0
  9. 2026Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version)cited by 0
  10. 2026Is Your Agent Playing Dead? Deployed LLM Agents Exhibit Constraint-Evasive Fabrication and Thanatosiscited by 0
  11. 2026Cycle-Consistent Neural Explanation of Formal Verification Certificatescited by 0
  12. 2026Shielding for Higher-Order Safetycited by 0