Quantitative safety and liveness LNCS Henzinger, Thomas A ; https://orcid.org/0000-0002-2985-7724 Mazzocchi, Nicolas Adrien Sarac, Naci E ddc:000 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. Springer Nature 2023 info:eu-repo/semantics/conferenceObject doc-type:conferenceObject text https://research-explorer.ista.ac.at/record/12467 https://research-explorer.ista.ac.at/download/12467/12468 https://research-explorer.ista.ac.at/download/12467/13153 Henzinger TA, Mazzocchi NA, Sarac NE. Quantitative safety and liveness. In: <i>26th International Conference Foundations of Software Science and Computation Structures</i>. Vol 13992. Springer Nature; 2023:349-370. doi:<a href="https://doi.org/10.1007/978-3-031-30829-1_17">10.1007/978-3-031-30829-1_17</a> eng info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-031-30829-1_17 info:eu-repo/semantics/altIdentifier/issn/0302-9743 info:eu-repo/semantics/altIdentifier/e-issn/1611-3349 info:eu-repo/semantics/altIdentifier/isbn/9783031308284 info:eu-repo/semantics/altIdentifier/wos/001288609300017 info:eu-repo/semantics/altIdentifier/arxiv/2301.11175 https://creativecommons.org/licenses/by/4.0/ info:eu-repo/semantics/openAccess