Multiplayer Games With Incomplete Information for Hyperproperty Verification

Hyperproperties are system properties that relate multiple execution traces in a system and can, e.g., express security policies, knowledge properties, path planning, and robustness requirements. Logics for expressing temporal hyperproperties-such as Hyper-LTL-extend LTL by quantifying over executions of a system. Many properties used in practice require one or more quantifier alternations, which presents a major challenge for verification. Complete verification methods require a system complementation for each quantifier alternation, making it infeasible in practice. A cheaper method interprets the verification of a HyperLTL formula as a twoplayer parity game between universal and existential quantifiers. This game-based approach is very efficient and allows for interactive proofs, but is limited to ∀ * ∃ * HyperLTL formulas, leaving important properties out of reach. In this paper, we argue that we can extend the game-based verification approach to arbitrary HyperLTL formulas, by utilizing multiple players and incomplete information.