@inproceedings{12467,
  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.},
  author       = {Henzinger, Thomas A and Mazzocchi, Nicolas Adrien and Sarac, Naci E},
  booktitle    = {26th International Conference Foundations of Software Science and Computation Structures},
  isbn         = {9783031308284},
  issn         = {1611-3349},
  location     = {Paris, France},
  pages        = {349--370},
  publisher    = {Springer Nature},
  title        = {{Quantitative safety and liveness}},
  doi          = {10.1007/978-3-031-30829-1_17},
  volume       = {13992},
  year         = {2023},
}