{"ID":2839188,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2511.16579","arxiv_id":"2511.16579","title":"Synthesis of Safety Specifications for Probabilistic Systems","abstract":"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.","short_abstract":"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 expre...","url_abs":"https://arxiv.org/abs/2511.16579","url_pdf":"https://arxiv.org/pdf/2511.16579v1","authors":"[\"Gaspard Ohlmann\",\"Edwin Hamel-De le Court\",\"Francesco Belardinelli\"]","published":"2025-11-20T17:34:56Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.AI\",\"cs.LG\",\"eess.SY\"]","methods":"[]","has_code":false}