Synthesis of Safety Specifications for Probabilistic Systems
This work addresses safety-critical environments by enabling more expressive safety specifications for probabilistic systems, representing an incremental advance over existing methods limited to probabilistic-avoidance constraints.
The paper tackles the problem of ensuring safety in probabilistic systems by developing a new approach that supports more general temporal properties expressed in Probabilistic Computation Tree Logic (PCTL), proposing a theoretical framework and a value iteration-based algorithm with proven soundness and completeness.
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.