Synthesis of Safety Specifications for Probabilistic Systems
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866912721376641024 |
|---|---|
| author | Ohlmann, Gaspard Court, Edwin Hamel-De le Belardinelli, Francesco |
| author_facet | Ohlmann, Gaspard Court, Edwin Hamel-De le Belardinelli, Francesco |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_16579 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Synthesis of Safety Specifications for Probabilistic Systems Ohlmann, Gaspard Court, Edwin Hamel-De le Belardinelli, Francesco Logic in Computer Science Artificial Intelligence Machine Learning Systems and Control 68Q60, 60J20, 68T05 F.3.1; F.4.1; I.2.6 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. |
| title | Synthesis of Safety Specifications for Probabilistic Systems |
| topic | Logic in Computer Science Artificial Intelligence Machine Learning Systems and Control 68Q60, 60J20, 68T05 F.3.1; F.4.1; I.2.6 |
| url | https://arxiv.org/abs/2511.16579 |