Safety and Liveness of Quantitative Properties and Automata

TL;DR

This work extends the classic boolean safety-liveness dichotomy to quantitative properties by treating properties as functions from infinite words to a complete lattice $\mathbb{D}$ and introducing quantitative safety, liveness, and their topological characterizations. It generalizes the safety-progress hierarchy via limit properties (Inf, Sup, LimInf, LimSup) and proves a universal safety-liveness decomposition: every property is the pointwise minimum of a safety closure and a live component; a dual co-safety/co-liveness decomposition also exists. The framework is instantiated for quantitative automata with common value functions ${\mathsf{Inf}}, {\mathsf{Sup}}, {\mathsf{LimInf}}, {\mathsf{LimSup}}, {\mathsf{LimInfAvg}}, {\mathsf{LimSupAvg}}, {\mathsf{DSum}}$, along with decision procedures to decide safety/liveness and construct safety closures, yielding PSPACE- or ExpSpace-complete results depending on the function. The results enable compositional monitorability analyses and practical decompositions, with several optimizations and a tool implementation mentioned, providing a robust pathway for quantitative verification and monitoring.

Abstract

Safety and liveness stand as fundamental concepts in formal languages, playing a key role in verification. 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 the quantitative setting, properties are arbitrary functions from infinite words to partially-ordered domains. Extending this paradigm to the quantitative domain, where properties are arbitrary functions mapping infinite words to partially-ordered domains, we introduce and study the notions of quantitative safety and liveness. First, we formally define quantitative safety and liveness, and prove that our definitions induce conservative quantitative generalizations of both the safety-progress hierarchy and the safety-liveness decomposition of boolean properties. Consequently, like their boolean counterparts, quantitative properties can be min-decomposed into safety and liveness parts, or alternatively, max-decomposed into co-safety and co-liveness parts. We further establish a connection between quantitative safety and topological continuity and provide alternative characterizations of quantitative safety and liveness in terms of their boolean analogs. Second, we instantiate our framework with the specific classes of quantitative properties expressed by automata. These quantitative automata contain finitely many states and rational-valued transition weights, and their common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the totally-ordered domain of real numbers. For all common value functions, we provide a procedure for deciding whether a given automaton is safe or live, we show how to construct its safety closure, and we present a min-decomposition into safe and live automata.

Figures (3)

• Figure 1: (a) A ${\mathsf{LimSup}}$-automaton $\mathcal{A}$ modeling the long-term maximal power consumption of a device. (b) An ${\mathsf{Inf}}$-automaton (or a ${\mathsf{LimSup}}$-automaton) expressing the safety closure of $\mathcal{A}$. (c) A ${\mathsf{LimSup}}$-automaton expressing the liveness component of the decomposition of $\mathcal{A}$.
• Figure 2: A ${\mathsf{Sup}}$-automaton $\mathcal{A}$ together with its safety closure $\mathcal{B}$ given as an ${\mathsf{Inf}}$-automaton, which cannot be expressed by a ${\mathsf{Sup}}$-automaton.
• Figure 3: A nondeterministic ${\mathsf{LimInfAvg}}$-automaton $\mathcal{A}$ and its safety-liveness decomposition into ${\mathsf{LimInfAvg}}$-automata $\mathcal{B}$ and $\mathcal{C}$, as presented in the proof of \ref{['cl:SafetyLivenessDecompositionLimAvg']}.

Theorems & Definitions (160)

• Definition 3.1: Safety
• Example 3.2
• Proposition 3.3
• proof
• Proposition 3.4
• proof
• Definition 3.5: Safety closure
• Theorem 3.6
• proof
• Remark 3.7