On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information
Raven Beutner, Bernd Finkbeiner · arXiv (Cornell University) · 2025
Hyperproperties generalize traditional trace properties by relating multiple execution traces rather than reasoning about individual runs in isolation.They provide au nified way toe xpress important requirements such as information flowa nd robustness properties.Temporal logics likeH yperLTL capture these properties by explicitly quantifying over executions of asystem.However, many practically relevant hyperproperties involve quantifier alternations,afeaturet hat poses substantial challenges forautomated verification.Complete verification methods require asystem complementation foreach quantifier alternation, making it infeasible in practice.Ac heaper (but incomplete) method interprets the verification of aHyperLTL formula as atwo-player game betweenu niversal and existential quantifiers.The gamebased approach is significantly cheaper,f acilitates interactive proofs, and allows fore asy-to-check certificates of satisfaction.It is, however, limited to ∀ * ∃ * properties, leaving important properties out of reach.In this paper,w eshowthat we can use games to verify hyperproperties with arbitrary quantifier alternations byu tilizing multiplayer games under partial information.W hile games under partiali nformation are, in general, undecidable, we showt hat our game is played under hierarchical information and thus falls in ad ecidable class of games.We discuss the completeness of the game and study prophecy variables in the setting of partial information.