# Value Functions as Supermartingale Certificates

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 27 of its 53 references that are in the map.
- First posted on arXiv 29 May 2026.

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

- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Omega-Regular Objectives in Model-Free Reinforcement Learning](https://mlsanity.com/paper/1810.00950/) (2018)
- [Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learning](https://mlsanity.com/paper/1909.07299/) (2019)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees](https://mlsanity.com/paper/2210.05308/) (2022)
- [On Convergence of Emphatic Temporal-Difference Learning](https://mlsanity.com/paper/1506.02582/) (2015)
- [Sample Efficient Model-free Reinforcement Learning from LTL Specifications with Optimality Guarantees](https://mlsanity.com/paper/2305.01381/) (2023)
- [Logically-Constrained Neural Fitted Q-Iteration](https://mlsanity.com/paper/1809.07823/) (2018)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)
- [LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning](https://mlsanity.com/paper/2209.10341/) (2022)
- [Stochastic Omega-Regular Verification and Control with Supermartingales](https://mlsanity.com/paper/2405.17304/) (2024)
- [Termination Analysis of Probabilistic Programs through Positivstellensatz's](https://mlsanity.com/paper/1604.07169/) (2016)
- [Stochastic Invariants for Probabilistic Termination](https://mlsanity.com/paper/1611.01063/) (2016)
- [Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints](https://mlsanity.com/paper/1804.08924/) (2018)
- [Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs](https://mlsanity.com/paper/1510.08517/) (2015)
- [Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems](https://mlsanity.com/paper/2404.01769/) (2024)
- [Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs](https://mlsanity.com/paper/1709.04037/) (2017)
- [Bisimulation Learning](https://mlsanity.com/paper/2405.15723/) (2024)
- [Quantitative Supermartingale Certificates](https://mlsanity.com/paper/2504.05065/) (2025)
- [Supermartingale Certificates for Quantitative Omega-regular Verification and Control](https://mlsanity.com/paper/2505.18833/) (2025)
- [Quantitative Verification with Neural Networks](https://mlsanity.com/paper/2301.06136/) (2023)
- [Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates](https://mlsanity.com/paper/2406.00826/) (2024)
- [Sound and Complete Proof Rules for Probabilistic Termination](https://mlsanity.com/paper/2404.19724/) (2024)
- [A Hierarchy of Supermartingales for ω-Regular Verification](https://mlsanity.com/paper/2512.00270/) (2025)
- [Composing Reinforcement Learning Policies, with Formal Guarantees](https://mlsanity.com/paper/2402.13785/) (2024)
- [Fixed Point Certificates for Reachability and Expected Rewards in MDPs](https://mlsanity.com/paper/2501.11467/) (2025)

## Abstract (arXiv)

Certification methods for stochastic systems provide sufficient proof rules, based on real-valued supermartingale certificates, to determine the almost-sure satisfaction of ω-regular properties (and therefore of linear temporal logic) over general state spaces, encompassing both countably infinite and continuous state spaces. Conversely, reinforcement learning (RL) methods for ω-regular tasks have received considerable attention, but they typically lack formal guarantees that the learned policy satisfies the specification, except possibly for finite state and action spaces. We bridge these two lines of research by establishing a novel theoretical connection: under an appropriate reward, the value function associated to a policy that almost surely satisfies an ω-regular property encodes a Streett supermartingale certificate for that specification. Our results, validated experimentally on finite Markov decision processes, hold for finite, countably infinite, and continuous state spaces, suggesting a principled route to certificate synthesis via RL.