Multiplayer Games With Incomplete Information for Hyperproperty Verification.

Summary

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 HyperLTL - 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 two-player 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.