Quantitative Safety and Liveness

TL;DR

This paper extends safety and liveness concepts to quantitative properties, providing a framework for their decomposition, approximation, and monitoring, thus generalizing classical boolean property classifications.

Contribution

It introduces definitions of quantitative safety and liveness, proving they generalize boolean classifications and enable decomposition and approximation of quantitative properties.

Findings

Every quantitative property can be decomposed into safety and liveness parts.

Quantitative properties with safe and co-safe approximations can be monitored precisely.

The framework generalizes classical boolean safety-liveness hierarchy to quantitative settings.

Abstract

Safety and liveness are elementary concepts of computation, and the foundation of many verification paradigms. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In quantitative specification and verification, properties assign not truth values, but quantitative values to infinite traces (e.g., a cost, or the distance to a boolean property). We introduce quantitative safety and liveness, and we prove that our definitions induce conservative quantitative generalizations of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness decomposition of boolean properties. In particular, we show that every quantitative property can be written as the pointwise minimum of a quantitative safety property and a quantitative liveness property. Consequently, like boolean properties, also quantitative properties can be $\min$-decomposed into safety and liveness parts, or alternatively, $\max$-decomposed into co-safety and co-liveness parts. Moreover, quantitative properties can be approximated naturally. We prove that every quantitative property that has both safe and co-safe approximations can be monitored arbitrarily precisely by a monitor that uses only a finite number of states.