Synthesis of Safety Specifications for Probabilistic Systems

TL;DR

This paper introduces a novel framework and algorithm for synthesizing safety specifications in probabilistic systems using a fragment of PCTL, enabling more expressive safety guarantees.

Contribution

It develops a theoretical framework for safe-PCTL synthesis, defines the CPCTL fragment, and proposes a value iteration algorithm with proven soundness and completeness.

Findings

Framework for safe-PCTL synthesis established

CPCTL fragment effectively captures safety properties

Algorithm demonstrated to be sound and complete

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.