定量超性质的统计验证：超越布尔量化
Statistical Verification of Quantitative Hyperproperties: Beyond Boolean Quantification
浏览论文内容
中文总结 AI 辅助
本文针对现有超性质形式体系无法处理系统定量特性的问题，提出定量超逻辑（QHL），开发其统计验证算法，结合统计方法为嵌套测度量词提供验证方案，在定量IFC基准上验证了方法的表达性与有效性。
中文摘要 AI 辅助
超性质形式体系为研究关系性质类别的验证问题提供了坚实基础，例如信息流控制（IFC）中的相关性质。然而，现有形式体系在捕捉现实系统的实际方面时表达能力有限，尤其未能充分考虑这类系统的定量特性。本文从定量、基于测度的视角重新探讨超性质的规范与验证，提出定量超逻辑（QHL），该逻辑用基于测度的迹量词替代定性迹量词，并为时间谓词扩展更丰富的定量表达式。我们进一步从统计验证角度研究该问题，开发针对QHL规范的统计验证算法；针对提出的基于测度的量词，我们特别在样本复杂度和可实现统计保证方面进行分析，展示如何结合Hoeffding不等式和极值理论等统计方法，为嵌套的基于测度的量词开发统计验证算法。在传统验证方法变得不可行的场景中，本文方法提供了定量替代方案；我们在定量IFC的基准测试上，通过与定性方法对比，验证了所提方法的表达能力和有效性。
英文摘要
Formalisms for hyperproperties provide a solid foundation for studying the verification problem across classes of relational properties, such as those in information flow control (IFC). However, existing formalisms remain limited in expressiveness when it comes to capturing practical aspects of real-world systems. In particular, they do not adequately account for the quantitative nature of such systems. In this paper, we address this gap by revisiting the specification and verification of hyperproperties from a quantitative, measure-based, perspective. We introduce Quantitative Hyper-Logic (QHL), which replaces qualitative trace quantifiers with measure-based ones and extends temporal predicates with richer quantitative expressions. We further study the verification problem from a statistical verification point of view, and develop algorithms for the statistical verification of QHL specifications. For the introduced measure-based quantifiers, we particularly provide an analysis in terms of sample complexity and achievable statistical guarantees. In particular, we show how statistical methods such as Hoeffding's inequality and extreme value theory can be combined to develop statistical verification algorithms for nested measure-based quantifiers. Our approach provides quantitative alternatives for where traditional verification methods become infeasible. We demonstrate both expressiveness and efficacy on benchmarks from quantitative IFC, comparing against qualitative methods.
