# Formal Policy Synthesis for Continuous-Space Systems via Reinforcement Learning

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 May 2020.

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

- [Modular Deep Reinforcement Learning for Continuous Motion Planning with Temporal Logic](https://mlsanity.com/paper/2102.12855/) (2021)
- [DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL](https://mlsanity.com/paper/2410.04631/) (2024)
- [Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings](https://mlsanity.com/paper/2403.10497/) (2024)
- [Safe Reach Set Computation via Neural Barrier Certificates](https://mlsanity.com/paper/2404.18813/) (2024)
- [Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification](https://mlsanity.com/paper/2407.21029/) (2024)
- [LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems](https://mlsanity.com/paper/2512.11750/) (2025)
- [Average Reward Reinforcement Learning for Omega-Regular and Mean-Payoff Objectives](https://mlsanity.com/paper/2505.15693/) (2025)
- [Kernel-Based Learning of Safety Barriers](https://mlsanity.com/paper/2601.12002/) (2026)

## Abstract (arXiv)

This paper studies satisfaction of temporal properties on unknown stochastic processes that have continuous state spaces. We show how reinforcement learning (RL) can be applied for computing policies that are finite-memory and deterministic using only the paths of the stochastic process. We address properties expressed in linear temporal logic (LTL) and use their automaton representation to give a path-dependent reward function maximised via the RL algorithm. We develop the required assumptions and theories for the convergence of the learned policy to the optimal policy in the continuous state space. To improve the performance of the learning on the constructed sparse reward function, we propose a sequential learning procedure based on a sequence of labelling functions obtained from the positive normal form of the LTL specification. We use this procedure to guide the RL algorithm towards a policy that converges to an optimal policy under suitable assumptions on the process. We demonstrate the approach on a 4-dim cart-pole system and 6-dim boat driving problem.