定量安全性与活性
摘要：安全性和活性是计算的基本概念，也是许多验证范例的基础。布尔属性的安全性活性分类描述了给定属性是否能通过观察无限计算轨迹的有限前缀来验证（对于安全性总是成立，而对于活性性质永远不成立）。在定量规范和验证中，属性为无限轨迹分配的不是真值，而是定量值（例如成本或与布尔属性的距离）。我们引入了定量安全性和活性性质，并证明我们的定义对于（1）布尔属性安全进展层次结构以及（2）布尔属性的安全性活性分解都产生了保守的定量概括。特别地，我们展示了每个定量属性都可以写成定量安全性属性和定量活性性质的逐点最小值。因此，类似布尔属性，定量属性也可以被分解为安全性和活性部分，或者被分解为反安全性和反活性部分。此外，定量属性可以自然地近似。我们证明了每个既有安全近似又有反-安全近似的定量属性都可以由只使用有限个状态的监控器任意精确地监测。
作者：Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sarac{c}
论文ID：2301.11175
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-25