Prophecy Variables for Hyperproperty Verification

TL;DR

This paper introduces a method to make game-based hyperproperty verification complete by incorporating $ ext{ω}$-regular temporal prophecies, enabling more accurate verification of properties with quantifier alternations.

Contribution

It presents a constructive approach to add temporal prophecies to game-based verification, making it complete for hyperproperties with quantifier alternations.

Findings

Game-based approach can be made complete with $ ext{ω}$-regular prophecies.

Constructive algorithm for generating a complete set of prophecies.

Enhanced verification accuracy for hyperproperties with quantifier alternations.

Abstract

Temporal logics for hyperproperties like HyperLTL use trace quantifiers to express properties that relate multiple system runs. In practice, the verification of such specifications is mostly limited to formulas without quantifier alternation, where verification can be reduced to checking a trace property over the self-composition of the system. Quantifier alternations like $\forall \pi. \exists \pi'. \phi$, can either be solved by complementation or with an interpretation as a two-person game between a $\forall$-player, who incrementally constructs the trace $\pi$, and an $\exists$-player, who constructs $\pi'$ in such a way that $\pi$ and $\pi'$ together satisfy $\phi$. The game-based approach is significantly cheaper but incomplete because the $\exists$-player does not know the future moves of the $\forall$-player. In this paper, we establish that the game-based approach can be made complete by adding ($\omega$-regular) temporal prophecies. Our proof is constructive, yielding an effective algorithm for the generation of a complete set of prophecies.