# Correct-by-synthesis reinforcement learning with temporal logic constraints

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Mar 2015.

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

- [Joint Learning of Reward Machines and Policies in Environments with Partially Known Semantics](https://mlsanity.com/paper/2204.11833/) (2022)
- [Probabilistic Planning with Preferences over Temporal Goals](https://mlsanity.com/paper/2103.14489/) (2021)
- [Efficient Reinforcement Learning in Probabilistic Reward Machines](https://mlsanity.com/paper/2408.10381/) (2024)
- [Assured Learning-enabled Autonomy: A Metacognitive Reinforcement Learning Framework](https://mlsanity.com/paper/2103.12558/) (2021)
- [Reinforcement Learning with Formal Performance Metrics for Quadcopter Attitude Control under Non-nominal Contexts](https://mlsanity.com/paper/2107.12942/) (2021)
- [Learning Performance Graphs from Demonstrations via Task-Based Evaluations](https://mlsanity.com/paper/2204.05909/) (2022)
- [Shielded Deep Reinforcement Learning for Complex Spacecraft Tasking](https://mlsanity.com/paper/2403.05693/) (2024)
- [Learning Gait-Aware Quadruped Locomotion with Temporal Logic Specifications](https://mlsanity.com/paper/2607.00442/) (2026)
- [On Satisficing in Quantitative Games](https://mlsanity.com/paper/2101.02594/) (2021)
- [Synthesis from Satisficing and Temporal Goals](https://mlsanity.com/paper/2205.10464/) (2022)
- [A Unified Approach to Multi-task Legged Navigation: Temporal Logic Meets Reinforcement Learning](https://mlsanity.com/paper/2407.06931/) (2024)

## Abstract (arXiv)

We consider a problem on the synthesis of reactive controllers that optimize some a priori unknown performance criterion while interacting with an uncontrolled environment such that the system satisfies a given temporal logic specification. We decouple the problem into two subproblems. First, we extract a (maximally) permissive strategy for the system, which encodes multiple (possibly all) ways in which the system can react to the adversarial environment and satisfy the specifications. Then, we quantify the a priori unknown performance criterion as a (still unknown) reward function and compute an optimal strategy for the system within the operating envelope allowed by the permissive strategy by using the so-called maximin-Q learning algorithm. We establish both correctness (with respect to the temporal logic specifications) and optimality (with respect to the a priori unknown performance criterion) of this two-step technique for a fragment of temporal logic specifications. For specifications beyond this fragment, correctness can still be preserved, but the learned strategy may be sub-optimal. We present an algorithm to the overall problem, and demonstrate its use and computational requirements on a set of robot motion planning examples.