Probabilistic Safety Guarantees for Markov Decision Processes

This article aims to incorporate safety specifications into Markov decision processes. Explicitly, we address the minimization problem up to a stopping time with safety constraints. We establish a formalism leaning upon the evolution equation to achieve our goal. We show how to compute the safety function with dynamic programming. In the last part of this article, we develop several algorithms for safe stochastic optimization using linear and dynamic programming.