Quantitative Safety and Liveness

23^rd November 2023, 11:00 Ashton 101
Nicolas Mazzocchi
IST Austria

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). For quantitative specification and verification, properties map an infinite trace to a value from a partially-ordered domain (not just truth values). First, we introduce quantitative safety and liveness that induce conservative quantitative generalizations of both the safety-progress hierarchy of Boolean properties and the safety-liveness decomposition of Boolean properties. Second, we look into harnessing the dichotomy for the specific classes of quantitative properties expressed by quantitative automata. These 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. In this automata-theoretic setting, we establish a connection between quantitative safety and topological continuity and provide an alternative characterization of quantitative safety and liveness in terms of their Boolean counterparts. For all common value functions, we show how the safety closure of a quantitative automaton can be constructed in PTime, and we provide PSpaceC checks of whether a given quantitative automaton is safe or live, with the exception of LimInfAvg and LimSupAvg automata, for which the safety check is in ExpSpace. Moreover, for deterministic Sup, LimInf, and LimSup automata, we give PTime decompositions into safe and live automata. These decompositions enable the separation of techniques for safety and liveness verification for quantitative specifications.