--- res: bibo_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.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Thomas A foaf_name: Henzinger, Thomas A foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0002-2985-7724 - foaf_Person: foaf_givenName: Nicolas Adrien foaf_name: Mazzocchi, Nicolas Adrien foaf_surname: Mazzocchi foaf_workInfoHomepage: http://www.librecat.org/personId=b26baa86-3308-11ec-87b0-8990f34baa85 - foaf_Person: foaf_givenName: Naci E foaf_name: Sarac, Naci E foaf_surname: Sarac foaf_workInfoHomepage: http://www.librecat.org/personId=8C6B42F8-C8E6-11E9-A03A-F2DCE5697425 bibo_doi: 10.1007/978-3-031-30829-1_17 bibo_volume: 13992 dct_date: 2023^xs_gYear dct_isPartOf: - http://id.crossref.org/issn/0302-9743 - http://id.crossref.org/issn/1611-3349 - http://id.crossref.org/issn/9783031308284 dct_language: eng dct_publisher: Springer Nature@ dct_title: Quantitative safety and liveness@ ...