# AutoHyper: Explicit-State Model Checking for HyperLTL

arXiv: https://arxiv.org/abs/2301.11229 · HTML: https://mlsanity.com/paper/2301.11229/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Jan 2023.

## Built on by (most cited first, 8 of 8)

- [Non-Deterministic Planning for Hyperproperty Verification](https://mlsanity.com/paper/2405.13488/) (2024)
- [On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing](https://mlsanity.com/paper/2312.12403/) (2023)
- [Counterfactuals Modulo Temporal Logics](https://mlsanity.com/paper/2306.08916/) (2023)
- [Hyper Strategy Logic](https://mlsanity.com/paper/2403.13741/) (2024)
- [Probabilistic Strategy Logic with Degrees of Observability](https://mlsanity.com/paper/2412.15135/) (2024)
- [Hyperproperty-Constrained Secure Reinforcement Learning](https://mlsanity.com/paper/2508.00106/) (2025)
- [An Information-Flow Perspective on Explainability Requirements: Specification and Verification](https://mlsanity.com/paper/2509.01479/) (2025)
- [On Conformant Planning and Model-Checking of exists^*forall^* Hyperproperties](https://mlsanity.com/paper/2512.23324/) (2025)

## Abstract (arXiv)

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.