一句话：将布尔安全-活性分类推广到定量性质，并为常见定量自动机给出安全/活性判定、安全闭包与分解。
本文把形式语言与验证中的安全性和活性从布尔性质推广到定量性质。定量性质是从无限字到偏序域的函数。作者形式化定义定量安全性和活性，证明它们保守推广布尔安全-进展谱系与安全-活性分解，并得到最小分解为安全/活性部分、最大分解为余安全/余活性部分的结果；还建立定量安全性与拓扑连续性的联系。论文还在有限状态、有理权重的定量自动机上实例化框架，对 Inf、Sup、LimInf、LimSup 及其平均和 DSum 等常见值函数，给出安全/活性判定、安全闭包构造和最小分解算法。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BokerHMS25,
title = {Safety and Liveness of Quantitative Properties and Automata},
author = {Udi Boker and Thomas A. Henzinger and Nicolas Mazzocchi and N. Ege Saraç},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 2},
year = {2025},
doi = {10.46298/lmcs-21(2:2)2025}
}