AutoHyper: leveraging language inclusion checking for hyperproperty model-checking

Abstract Hyperproperties are system properties that relate multiple execution traces, and naturally occur, e.g., in information-flow control, knowledge, robustness, mutation testing, path planning, and causality checking. HyperLTL is a temporal logic that can express complex temporal hyperproperties by extending LTL with quantification over execution traces. 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. In this paper, we present , an explicit-state automata-based model checker for HyperLTL that is complete for formulas with an arbitrary quantifier prefix. On the theoretical side, we show how language inclusion checks between $\omega $ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>ω</mml:mi> </mml:math> -automata can be integrated into HyperLTL verification. On the practical side, this allows to leverage a range of existing inclusion-checking tools for hyperproperty verification. We further extend our model-checking algorithm to support HyperLTL modulo theories, i.e., formulas where the atomic formulas consist of first-order formulas instead of Boolean atomic propositions. We show how we can model-check such formulas effectively by tracking partially evaluated first-order formulas within an automaton. We evaluate on a broad set of benchmarks drawn from different areas in the literature and compare it with existing (incomplete) methods for HyperLTL verification.