# LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 46 references that are in the map.
- First posted on arXiv 21 Sep 2022.

## Builds on (most cited first, 21 of 21)

- [DeepMind Control Suite](https://mlsanity.com/paper/1801.00690/) (2018)
- [Modular Multitask Reinforcement Learning with Policy Sketches](https://mlsanity.com/paper/1611.01796/) (2016)
- [Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees](https://mlsanity.com/paper/1909.05304/) (2019)
- [Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learning](https://mlsanity.com/paper/1909.07299/) (2019)
- [Foundations for Restraining Bolts: Reinforcement Learning with LTLf/LDLf restraining specifications](https://mlsanity.com/paper/1807.06333/) (2018)
- [A Composable Specification Language for Reinforcement Learning Tasks](https://mlsanity.com/paper/2008.09293/) (2020)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Logically-Constrained Reinforcement Learning](https://mlsanity.com/paper/1801.08099/) (2018)
- [A Learning Based Approach to Control Synthesis of Markov Decision Processes for Linear Temporal Logic Specifications](https://mlsanity.com/paper/1409.5486/) (2014)
- [Cautious Reinforcement Learning with Logical Constraints](https://mlsanity.com/paper/2002.12156/) (2020)
- [Modular Deep Reinforcement Learning for Continuous Motion Planning with Temporal Logic](https://mlsanity.com/paper/2102.12855/) (2021)
- [Certified Reinforcement Learning with Logic Guidance](https://mlsanity.com/paper/1902.00778/) (2019)
- [Verifiably Safe Exploration for End-to-End Reinforcement Learning](https://mlsanity.com/paper/2007.01223/) (2020)
- [Rethinking the Discount Factor in Reinforcement Learning: A Decision Theoretic Approach](https://mlsanity.com/paper/1902.02893/) (2019)
- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [Logically-Constrained Neural Fitted Q-Iteration](https://mlsanity.com/paper/1809.07823/) (2018)
- [Verifiably Safe Off-Model Reinforcement Learning](https://mlsanity.com/paper/1902.05632/) (2019)
- [FAUST2: Formal Abstractions of Uncountable-STate STochastic processes](https://mlsanity.com/paper/1403.3286/) (2014)
- [DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning](https://mlsanity.com/paper/1911.10244/) (2019)
- [Formal Consistency Checking over Specifications in Natural Languages](https://mlsanity.com/paper/1405.5003/) (2014)
- [Mungojerrie: Reinforcement Learning of Linear-Time Objectives](https://mlsanity.com/paper/2106.09161/) (2021)

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

- [ALLURE: Auditing and Improving LLM-based Evaluation of Text using Iterative In-Context-Learning](https://mlsanity.com/paper/2309.13701/) (2023)
- [Sample-Efficient Reinforcement Learning with Temporal Logic Objectives: Leveraging the Task Specification to Guide Exploration](https://mlsanity.com/paper/2410.12136/) (2024)
- [Mission-driven Exploration for Accelerated Deep Reinforcement Learning with Temporal Logic Task Specifications](https://mlsanity.com/paper/2311.17059/) (2023)
- [Co-learning Planning and Control Policies Constrained by Differentiable Logic Specifications](https://mlsanity.com/paper/2303.01346/) (2023)
- [System III: Learning with Domain Knowledge for Safety Constraints](https://mlsanity.com/paper/2304.11593/) (2023)
- [Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions](https://mlsanity.com/paper/2602.06746/) (2026)
- [Probabilistic Counterexample Guidance for Safer Reinforcement Learning (Extended Version)](https://mlsanity.com/paper/2307.04927/) (2023)
- [Verified Compositional Neuro-Symbolic Control for Stochastic Systems with Temporal Logic Tasks](https://mlsanity.com/paper/2311.10863/) (2023)
- [Autonomous Learning From Success and Failure: Goal-Conditioned Supervised Learning with Negative Feedback](https://mlsanity.com/paper/2509.03206/) (2025)
- [Automating the Refinement of Reinforcement Learning Specifications](https://mlsanity.com/paper/2512.01047/) (2025)
- [Value Functions as Supermartingale Certificates](https://mlsanity.com/paper/2605.31524/) (2026)

## Abstract (arXiv)

LCRL is a software tool that implements model-free Reinforcement Learning (RL) algorithms over unknown Markov Decision Processes (MDPs), synthesising policies that satisfy a given linear temporal specification with maximal probability. LCRL leverages partially deterministic finite-state machines known as Limit Deterministic Buchi Automata (LDBA) to express a given linear temporal specification. A reward function for the RL algorithm is shaped on-the-fly, based on the structure of the LDBA. Theoretical guarantees under proper assumptions ensure the convergence of the RL algorithm to an optimal policy that maximises the satisfaction probability. We present case studies to demonstrate the applicability, ease of use, scalability, and performance of LCRL. Owing to the LDBA-guided exploration and LCRL model-free architecture, we observe robust performance, which also scales well when compared to standard RL approaches (whenever applicable to LTL specifications). Full instructions on how to execute all the case studies in this paper are provided on a GitHub page that accompanies the LCRL distribution www.github.com/grockious/lcrl.