Multiplayer Games With Incomplete Information for Hyperproperty Verification (Extended Abstract)

Raven Beutner and Bernd Finkbeiner

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.

International Conference on Autonomous Agents and Multiagent Systems May 2025
Contact Data Privacy Policy Imprint
Home People Publications
More