Safety and Liveness of Quantitative Properties and Automata
CoRR(2023)
摘要
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. 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. In this automata-theoretic setting, we establish a connection between
quantitative safety and topological continuity and provide alternative
characterizations of quantitative safety and liveness in terms of their boolean
analogs. 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.
更多查看译文
关键词
quantitative automata,safety,liveness
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要