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.

翻译：安全性与活性是计算的基本概念，也是许多验证范式的基础。布尔属性的安全性-活性分类刻画了给定属性是否可以通过观察无限计算轨迹的有限前缀来证伪（安全性总是可以，活性则永远不能）。在定量规约与验证中，属性分配给无限轨迹的不是真值，而是定量值（例如代价，或到布尔属性的距离）。我们提出了定量安全性与活性的概念，并证明我们的定义诱导了（1）布尔属性的安全性-进展层次结构以及（2）布尔属性的安全性-活性分解两者的保守定量推广。特别地，我们证明每个定量属性都可写为定量安全性属性与定量活性属性的逐点最小值。因此，与布尔属性类似，定量属性也可以被min-分解为安全性部分与活性部分，或者替代性地被max-分解为共安全性（co-safety）部分与共活性（co-liveness）部分。此外，定量属性可以被自然地近似。我们证明：每个同时具有安全近似与共安全近似的定量属性，都可以通过仅使用有限状态的监视器以任意精度进行监视。