2023/01/26 by Raven Beutner, Bernd Finkbeiner, Beutner, Raven +1 · 6 citations
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Model-Driven Software Engineering Techniques #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.2301.11229
openalex publication_date 2023/01/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.