# Verifiable and Compositional Reinforcement Learning Systems

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

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 33 references that are in the map.
- First posted on arXiv 7 Jun 2021.

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

- [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)
- [SPOTTER: Extending Symbolic Planning Operators through Targeted Reinforcement Learning](https://mlsanity.com/paper/2012.13037/) (2020)
- [Synthesis in pMDPs: A Tale of 1001 Parameters](https://mlsanity.com/paper/1803.02884/) (2018)

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

- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)
- [Learning Task Automata for Reinforcement Learning using Hidden Markov Models](https://mlsanity.com/paper/2208.11838/) (2022)
- [Ablation Study of How Run Time Assurance Impacts the Training and Performance of Reinforcement Learning Agents](https://mlsanity.com/paper/2207.04117/) (2022)
- [Categorical semantics of compositional reinforcement learning](https://mlsanity.com/paper/2208.13687/) (2022)
- [Verifiable Reinforcement Learning Systems via Compositionality](https://mlsanity.com/paper/2309.06420/) (2023)
- [Efficient Sensitivity Analysis for Parametric Robust Markov Chains](https://mlsanity.com/paper/2305.01473/) (2023)
- [Compositional shield synthesis for safe reinforcement learning in partial observability](https://mlsanity.com/paper/2509.12085/) (2025)
- [Handling Long and Richly Constrained Tasks through Constrained Hierarchical Reinforcement Learning](https://mlsanity.com/paper/2302.10639/) (2023)
- [Verified Compositional Neuro-Symbolic Control for Stochastic Systems with Temporal Logic Tasks](https://mlsanity.com/paper/2311.10863/) (2023)
- [A Multifidelity Sim-to-Real Pipeline for Verifiable and Compositional Reinforcement Learning](https://mlsanity.com/paper/2312.01249/) (2023)
- [A Unified Theory of Compositionality, Modularity, and Interpretability in Markov Decision Processes](https://mlsanity.com/paper/2506.09499/) (2025)
- [Automating the Refinement of Reinforcement Learning Specifications](https://mlsanity.com/paper/2512.01047/) (2025)
- [Realizable Abstractions: Near-Optimal Hierarchical Reinforcement Learning](https://mlsanity.com/paper/2512.04958/) (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 (pMDP) which is used to plan and to analyze compositions of subsystems, and of the collection of low-level subsystems themselves. 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; if they each learn a policy satisfying the appropriate 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 pMDP, 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. As an additional benefit, this procedure allows for particularly challenging or important components of an overall task to be determined automatically, and focused on, during training. Experimental results demonstrate the presented framework's novel capabilities.