# Synthesis of Safety Specifications for Probabilistic Systems

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 17 references that are in the map.
- First posted on arXiv 20 Nov 2025.

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

- [Probably Safe or Live](https://mlsanity.com/paper/1401.7171/) (2014)
- [Strategy Synthesis for Global Window PCTL](https://mlsanity.com/paper/2204.14107/) (2022)

## Abstract (arXiv)

Ensuring that agents satisfy safety specifications can be crucial in safety-critical environments. While methods exist for controller synthesis with safe temporal specifications, most existing methods restrict safe temporal specifications to probabilistic-avoidance constraints. Formal methods typically offer more expressive ways to express safety in probabilistic systems, such as Probabilistic Computation Tree Logic (PCTL) formulas. Thus, in this paper, we develop a new approach that supports more general temporal properties expressed in PCTL. Our contribution is twofold. First, we develop a theoretical framework for the Synthesis of safe-PCTL specifications. We show how the reducing global specification satisfaction to local constraints, and define CPCTL, a fragment of safe-PCTL. We demonstrate how the expressiveness of CPCTL makes it a relevant fragment for the Synthesis Problem. Second, we leverage these results and propose a new Value Iteration-based algorithm to solve the synthesis problem for these more general temporal properties, and we prove the soundness and completeness of our method.