定量性质与自动机的安全性和活性
形式语言与自动机理论
2025-04-16 v6
摘要
安全性和活性是形式语言中的基本概念，在验证中起着关键作用。布尔性质的安全性-活性分类刻画了给定性质是否可通过观察无限计算轨迹的有限前缀来证伪（安全性总是可以，活性永远不可以）。在定量设定中，性质是从无限词到偏序域的任意函数。将这一范式扩展到定量领域，其中性质是将无限词映射到偏序域的任意函数，我们引入并研究了定量安全性和活性的概念。首先，我们形式化定义定量安全性和活性，并证明我们的定义给出了布尔性质的安全-进展层次结构和安全-活性分解的保守定量推广。因此，与布尔对应物类似，定量性质可最小分解（min-decomposed）为安全性和活性部分，或者可最大分解（max-decomposed）为协安全性和协活性部分。我们进一步建立了定量安全性与拓扑连续性之间的联系，并依据其布尔类比给出了定量安全性和活性的另类刻画。其次，我们用由自动机表达的特定定量性质类来实例化我们的框架。这些定量自动机包含有限个状态和有理值转移权重，其常用值函数 Inf、Sup、LimInf、LimSup、LimInfAvg、LimSupAvg 和 DSum 将无限词映射到全序实数域。对于所有常用值函数，我们给出了判定给定自动机是安全的还是活性的过程，展示了如何构造其安全性闭包，并给出了分解为安全与活性自动机的最小分解。
引用
@article{arxiv.2307.06016,
title = {Safety and Liveness of Quantitative Properties and Automata},
author = {Udi Boker and Thomas A. Henzinger and Nicolas Mazzocchi and N. Ege Saraç},
journal= {arXiv preprint arXiv:2307.06016},
year = {2025}
}