Formal Methods in AI Rigorous foundations for trustworthy intelligent systems
← Back to News

Tutorial AAMAS 2026: Formal Methods for Safe Reinforcement Learning

Dr. Edwin Hamel-De le Court, Alex W. Goodall, Dr. Francesco Belardinelli

Tutorial Description

The goal of the tutorial is to present the emerging relationship between Reinforcement Learning (RL) and Temporal Logic (TL). The topic is an active area of research that builds a bridge between the RL and verification communities. In a world where the safety of AI systems is becoming increasingly critical, bridging the gap between these communities is an important step toward developing safe, reliable, and trustworthy AI.

The tutorial is designed to appeal both to researchers in RL who want to understand how formal specifications can be used, and to researchers in formal methods who want to know how RL can help compute policies satisfying such specifications. Thus, the basics of both RL and TL will be carefully explained, and the tutorial will be comprehensible to a broad audience.

At the end of the tutorial, the audience will have the basics of RL and safe RL, a good intuition of the properties expressible in Temporal Logic, an understanding of TL model checking and reactive synthesis, and a clear overview of how these tools can be used to design RL algorithms with TL objectives or constraints, including methods that provide formal guarantees.

Tutorial Outline

  • Background: RL
    • Introduction to the main RL problem and standard algorithms such as DQN and PPO.
    • Introduction to constrained RL, including PPO-Lagrangian and CPO, and discussion of their limitations.
  • Background: Temporal Logic
    • Introduction to Linear Temporal Logic (LTL).
    • Automata over infinite words and translation from LTL to automata.
    • LTL model checking.
    • Synthesis for LTL safety specifications.
    • Probabilistic LTL and extensions of model checking.
  • RL with LTL objectives: how the problem differs from classical RL, and methods to address infinite horizons and sparse rewards.
  • Constrained RL with LTL constraints: shielding and related methods for obtaining safety guarantees when safety dynamics are known.

Presenters

Dr. Francesco Belardinelli is Senior Lecturer at the Department of Computing, Imperial College London (ICL), where he is head of the lab on Formal Methods in AI. He is also deputy director of the UKRI CDT in Safe and Trusted AI.

Dr. Edwin Hamel-De le Court is a postdoc at the University of Manchester. He is an expert in Formal Methods and Safe Reinforcement Learning; his research currently focuses on certifying the safety of autonomous agents.

Alex W. Goodall is a PhD student at the Department of Computing, Imperial College London (ICL). He is an expert in Safe Reinforcement Learning; his research currently focuses on shielding mechanisms that enforce the safety of Reinforcement Learning agents.

References

  1. Mnih et al. Playing Atari with Deep Reinforcement Learning. CoRR abs/1312.5602 (2013).
  2. Schulman et al. Proximal Policy Optimization Algorithms. CoRR abs/1707.06347 (2017).
  3. Achiam and Amodei. Benchmarking Safe Exploration in Deep Reinforcement Learning (2019).
  4. Achiam et al. Constrained Policy Optimization. ICML 2017.
  5. Baier and Katoen. Principles of Model Checking. MIT Press, 2008.
  6. Brazdil et al. Learning Algorithms for Verification of Markov Decision Processes. CoRR abs/2403.09184 (2024).
  7. Hasanbeig, Kroening, and Abate. Deep Reinforcement Learning with Temporal Logics. FORMATS 2020.
  8. Alshiekh et al. Safe Reinforcement Learning via Shielding. AAAI 2018.
  9. Hamel-De le Court et al. Probabilistic Shielding for Safe Reinforcement Learning. AAAI 2025.
© 2025-2026 Formal Methods in AI