# Prophecies all the Way: Game-based Model-Checking for HyperQPTL beyond forall^*exists^*

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Apr 2025.

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

- [On Conformant Planning and Model-Checking of exists^*forall^* Hyperproperties](https://mlsanity.com/paper/2512.23324/) (2025)

## Abstract (arXiv)

Model-checking HyperLTL, a temporal logic expressing properties of sets of traces with applications to information-flow based security and privacy, has a decidable, but TOWER-complete, model-checking problem. While the classical model-checking algorithm for full HyperLTL is automata-theoretic, more recently, a game-based alternative for the forall^*exists^*-fragment has been presented. Here, we employ imperfect information-games to extend the game-based approach to full HyperQPTL, which features arbitrary quantifier prefixes and quantification over propositions and can express every ω-regular hyperproperty. As a byproduct of our game-based algorithm, we obtain finite-state implementations of Skolem functions via transducers with lookahead that explain satisfaction or violation of HyperQPTL properties.