# Robust Dynamic Programming for Temporal Logic Control of Stochastic Systems

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Nov 2018.

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

- [Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification](https://mlsanity.com/paper/2407.21029/) (2024)
- [Robust optimal policies for team Markov games](https://mlsanity.com/paper/2105.07405/) (2021)
- [Transfer Learning for Control Systems via Neural Simulation Relations](https://mlsanity.com/paper/2412.01783/) (2024)
- [Average Reward Reinforcement Learning for Omega-Regular and Mean-Payoff Objectives](https://mlsanity.com/paper/2505.15693/) (2025)

## Abstract (arXiv)

Discrete-time stochastic systems are an essential modelling tool for many engineering systems. We consider stochastic control systems that are evolving over continuous spaces. For this class of models, methods for the formal verification and synthesis of control strategies are computationally hard and generally rely on the use of approximate abstractions. Building on approximate abstractions, we compute control strategies with lower- and upper-bounds for satisfying unbounded temporal logic specifications. Firstly, robust dynamic programming mappings over the abstract system are introduced to solve the control synthesis and verification problem. These mappings yield a control strategy and a unique lower bound on the satisfaction probability for temporal logic specifications that is robust to the incurred approximation errors. Secondly, upper-bounds on the satisfaction probability are quantified, and properties of the mappings are analysed and discussed. Finally, we show the implications of these results for linear stochastic dynamic systems with a continuous state space. This abstraction-based synthesis framework is shown to be able to handle infinite-horizon properties. Approximation errors expressed as deviations in the outputs of the models and as deviations in the probabilistic transitions are allowed and are quantified using approximate stochastic simulation relations.