Probably Safe or Live

TL;DR

This paper formalizes safety and liveness properties for probabilistic systems, providing algorithms and fragments of PCTL to characterize and decompose these properties, with insights into counterexamples and comparisons to existing frameworks.

Contribution

It introduces a formal characterization of safety and liveness in probabilistic systems, along with algorithms and PCTL fragments for property decomposition and classification.

Findings

Any probabilistic property can be decomposed into safety and liveness components.

Finite counterexamples exist for safety properties, none for liveness.

New PCTL fragments are identified for sound and complete safety and liveness characterization.

Abstract

This paper presents a formal characterisation of safety and liveness properties \`a la Alpern and Schneider for fully probabilistic systems. As for the classical setting, it is established that any (probabilistic tree) property is equivalent to a conjunction of a safety and liveness property. A simple algorithm is provided to obtain such property decomposition for flat probabilistic CTL (PCTL). A safe fragment of PCTL is identified that provides a sound and complete characterisation of safety properties. For liveness properties, we provide two PCTL fragments, a sound and a complete one. We show that safety properties only have finite counterexamples, whereas liveness properties have none. We compare our characterisation for qualitative properties with the one for branching time properties by Manolios and Trefler, and present sound and complete PCTL fragments for characterising the notions of strong safety and absolute liveness coined by Sistla.