# Verifiable Reinforcement Learning Systems via Compositionality

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 37 references that are in the map.
- First posted on arXiv 9 Sep 2023.

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

- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Data-Efficient Hierarchical Reinforcement Learning](https://mlsanity.com/paper/1805.08296/) (2018)
- [FeUdal Networks for Hierarchical Reinforcement Learning](https://mlsanity.com/paper/1703.01161/) (2017)
- [Hierarchical Deep Reinforcement Learning: Integrating Temporal Abstraction and Intrinsic Motivation](https://mlsanity.com/paper/1604.06057/) (2016)
- [Unity: A General Platform for Intelligent Agents](https://mlsanity.com/paper/1809.02627/) (2018)
- [Reward Machines: Exploiting Reward Function Structure in Reinforcement Learning](https://mlsanity.com/paper/2010.03950/) (2020)
- [Omega-Regular Objectives in Model-Free Reinforcement Learning](https://mlsanity.com/paper/1810.00950/) (2018)
- [Environment-Independent Task Specifications via GLTL](https://mlsanity.com/paper/1704.04341/) (2017)
- [Joint Inference of Reward Machines and Policies for Reinforcement Learning](https://mlsanity.com/paper/1909.05912/) (2019)
- [Reward Machines for Cooperative Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2007.01962/) (2020)
- [Induction and Exploitation of Subgoal Automata for Reinforcement Learning](https://mlsanity.com/paper/2009.03855/) (2020)
- [SPOTTER: Extending Symbolic Planning Operators through Targeted Reinforcement Learning](https://mlsanity.com/paper/2012.13037/) (2020)
- [Parameter Synthesis for Markov Models: Covering the Parameter Space](https://mlsanity.com/paper/1903.07993/) (2019)
- [Verifiable and Compositional Reinforcement Learning Systems](https://mlsanity.com/paper/2106.05864/) (2021)
- [Synthesis in pMDPs: A Tale of 1001 Parameters](https://mlsanity.com/paper/1803.02884/) (2018)

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

- [Compositional shield synthesis for safe reinforcement learning in partial observability](https://mlsanity.com/paper/2509.12085/) (2025)
- [VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change](https://mlsanity.com/paper/2505.14001/) (2025)
- [Automating the Refinement of Reinforcement Learning Specifications](https://mlsanity.com/paper/2512.01047/) (2025)

## Abstract (arXiv)

We propose a framework for verifiable and compositional reinforcement learning (RL) in which a collection of RL subsystems, each of which learns to accomplish a separate subtask, are composed to achieve an overall task. The framework consists of a high-level model, represented as a parametric Markov decision process, which is used to plan and analyze compositions of subsystems, and of the collection of low-level subsystems themselves. The subsystems are implemented as deep RL agents operating under partial observability. By defining interfaces between the subsystems, the framework enables automatic decompositions of task specifications, e.g., reach a target set of states with a probability of at least 0.95, into individual subtask specifications, i.e. achieve the subsystem's exit conditions with at least some minimum probability, given that its entry conditions are met. This in turn allows for the independent training and testing of the subsystems. We present theoretical results guaranteeing that if each subsystem learns a policy satisfying its subtask specification, then their composition is guaranteed to satisfy the overall task specification. Conversely, if the subtask specifications cannot all be satisfied by the learned policies, we present a method, formulated as the problem of finding an optimal set of parameters in the high-level model, to automatically update the subtask specifications to account for the observed shortcomings. The result is an iterative procedure for defining subtask specifications, and for training the subsystems to meet them. Experimental results demonstrate the presented framework's novel capabilities in environments with both full and partial observability, discrete and continuous state and action spaces, as well as deterministic and stochastic dynamics.