# Verification of general Markov decision processes by approximate similarity relations and policy refinement

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 May 2016.

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

- [Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions](https://mlsanity.com/paper/2301.01526/) (2023)
- [Correct-by-construction reach-avoid control of partially observable linear stochastic systems](https://mlsanity.com/paper/2103.02398/) (2021)
- [Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates (Extended Version)](https://mlsanity.com/paper/2506.16971/) (2025)
- [Neural Proofs for Sound Verification and Control of Complex Systems](https://mlsanity.com/paper/2512.18389/) (2025)
- [Safety Certification is Classification](https://mlsanity.com/paper/2605.06087/) (2026)

## Abstract (arXiv)

In this work we introduce new approximate similarity relations that are shown to be key for policy (or control) synthesis over general Markov decision processes. The models of interest are discrete-time Markov decision processes, endowed with uncountably-infinite state spaces and metric output (or observation) spaces. The new relations, underpinned by the use of metrics, allow in particular for a useful trade-off between deviations over probability distributions on states, and distances between model outputs. We show that the new probabilistic similarity relations, inspired by a notion of simulation developed for finite-state models, can be effectively employed over general Markov decision processes for verification purposes, and specifically for control refinement from abstract models.