HyperLTL is a temporal logic that can express hyperproperties, i.e., properties that relate multiple execution traces of a system. Such properties are becoming increasingly important and naturally occur, e.g., in information-flow control, robustness, mutation testing, path planning, and causality checking. Thus far, complete model checking tools for HyperLTL have been limited to alternation-free formulas, i.e., formulas that use only universal or only existential trace quantification. Properties involving quantifier alternations could only be handled in an incomplete way, i.e., the verification might fail even though the property holds. In this paper, we present AutoHyper, an explicit-state automata-based model checker that supports full HyperLTL and is complete for properties with arbitrary quantifier alternations. We show that language inclusion checks can be integrated into HyperLTL verification, which allows AutoHyper to benefit from a range of existing inclusion-checking tools. We evaluate AutoHyper on a broad set of benchmarks drawn from different areas in the literature and compare it with existing (incomplete) methods for HyperLTL verification.

翻译：HyperLTL是一种能够表达超性质的时间逻辑，即描述系统多条执行轨迹之间关系的性质。此类性质在信息流控制、鲁棒性分析、变异测试、路径规划及因果性检测等领域日益重要且自然存在。目前，针对HyperLTL的完备模型检测工具仅限于无交替公式，即仅使用全称或仅使用存在性迹量化的公式。涉及量词交替的性质只能以不完备方式处理，即即便性质成立，验证仍可能失败。本文提出AutoHyper——一种基于显式状态自动机的模型检测器，支持完整HyperLTL，并对任意量词交替的性质保持完备性。我们证明语言包含检查可集成至HyperLTL验证中，使AutoHyper能受益于现有多种包含检查工具。基于文献中多个领域的基准测试集，我们评估了AutoHyper，并与现有（不完备的）HyperLTL验证方法进行了对比。