Quantitative safety and liveness

DOI10.1007/978-3-031-30829-1_17MaRDI QIDQ6091203zbMATH OpenFDO

Authors Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Saraç

Publication date 24 November 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2301.11175

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

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.

Cites work

• A theory of register monitors
• Adequate proof principles for invariance and liveness properties of concurrent programs
• Approximate determinization of quantitative automata
• Automata, Languages and Programming
• Average-energy games
• Better Quality in Synthesis through Quantitative Objectives
• Bidirectional nested weighted automata
• Comparing LTL semantics for runtime verification
• Defining liveness
• Exact and approximate determinization of discounted-sum automata
• From model checking to model measuring
• Generalized quantitative analysis of metric transition systems
• Graph Games and Reactive Synthesis
• scientific article; zbMATH DE number 1982198 (Why is no real title available?)
• scientific article; zbMATH DE number 2038772 (Why is no real title available?)
• scientific article; zbMATH DE number 2080059 (Why is no real title available?)
• scientific article; zbMATH DE number 7650833 (Why is no real title available?)
• Model checking discounted temporal properties
• Model checking of linear-time properties in multi-valued systems
• Model checking of safety properties
• Probably safe or live
• Proving the Correctness of Multiprocess Programs
• Quantitative analysis of weighted transition systems
• Quantitative languages
• Recognizing safety and liveness
• Refining the safety-liveness classification of temporal properties according to monitorability
• Safety, liveness and fairness in temporal logic
• Simulation distances
• Spanning the spectrum from safety to liveness
• Temporal specifications with accumulative values
• The quantitative linear-time-branching-time spectrum
• Weighted safety

Cited in

(8)

• Safety, domain independence and generalized quantification
• Spanning the Spectrum from Safety to Liveness
• Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations
• Strategic dominance: a new preorder for nondeterministic processes
• Semantics for linear-time temporal logic with finite observations
• Safety and liveness of quantitative automata
• Safety and liveness of quantitative properties and automata
• Quantitative language automata

This page was built for publication: Quantitative safety and liveness

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6091203)