Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information

Raven Beutner, Bernd Finkbeiner

TL;DR

The paper tackles the verification of hyperproperties expressed in HyperLTL with arbitrary quantifier alternations by introducing multiplayer parity games under partial information (MPG$_{ii}$). It shows how to encode HyperLTL satisfaction as a game where players control traces, with observations aligned to the quantifier prefix, and proves soundness and decidability under hierarchical information. Completeness is established for the $\exists^*\forall^*$ fragment, and prophecy variables are developed to extend the framework to broader prefixes, yielding a sound-and-certificate approach for interactive proofs. The framework supports interactive proof construction, easy-to-check certificates, and broad applicability to hyperproperty verification, with future work exploring completeness for broader prefixes and practical solver integration.

Abstract

Hyperproperties generalize traditional trace properties by relating multiple execution traces rather than reasoning about individual runs in isolation. They provide a unified way to express important requirements such as information flow and robustness properties. Temporal logics like HyperLTL capture these properties by explicitly quantifying over executions of a system. However, many practically relevant hyperproperties involve quantifier alternations, a feature that poses substantial challenges for automated verification. Complete verification methods require a system complementation for each quantifier alternation, making it infeasible in practice. A cheaper (but incomplete) method interprets the verification of a HyperLTL formula as a two-player game between universal and existential quantifiers. The game-based approach is significantly cheaper, facilitates interactive proofs, and allows for easy-to-check certificates of satisfaction. It is, however, limited to $\forall^*\exists^*$ properties, leaving important properties out of reach. In this paper, we show that we can use games to verify hyperproperties with arbitrary quantifier alternations by utilizing multiplayer games under partial information. While games under partial information are, in general, undecidable, we show that our game is played under hierarchical information and thus falls in a decidable class of games. We discuss the completeness of the game and study prophecy variables in the setting of partial information.

On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information

TL;DR

The paper tackles the verification of hyperproperties expressed in HyperLTL with arbitrary quantifier alternations by introducing multiplayer parity games under partial information (MPG). It shows how to encode HyperLTL satisfaction as a game where players control traces, with observations aligned to the quantifier prefix, and proves soundness and decidability under hierarchical information. Completeness is established for the fragment, and prophecy variables are developed to extend the framework to broader prefixes, yielding a sound-and-certificate approach for interactive proofs. The framework supports interactive proof construction, easy-to-check certificates, and broad applicability to hyperproperty verification, with future work exploring completeness for broader prefixes and practical solver integration.

Abstract

Hyperproperties generalize traditional trace properties by relating multiple execution traces rather than reasoning about individual runs in isolation. They provide a unified way to express important requirements such as information flow and robustness properties. Temporal logics like HyperLTL capture these properties by explicitly quantifying over executions of a system. However, many practically relevant hyperproperties involve quantifier alternations, a feature that poses substantial challenges for automated verification. Complete verification methods require a system complementation for each quantifier alternation, making it infeasible in practice. A cheaper (but incomplete) method interprets the verification of a HyperLTL formula as a two-player game between universal and existential quantifiers. The game-based approach is significantly cheaper, facilitates interactive proofs, and allows for easy-to-check certificates of satisfaction. It is, however, limited to properties, leaving important properties out of reach. In this paper, we show that we can use games to verify hyperproperties with arbitrary quantifier alternations by utilizing multiplayer games under partial information. While games under partial information are, in general, undecidable, we show that our game is played under hierarchical information and thus falls in a decidable class of games. We discuss the completeness of the game and study prophecy variables in the setting of partial information.

Paper Structure

This paper contains 21 sections, 11 theorems, 18 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Game-Based Verification of $\forall^*\exists^*$
  4. Parity Games
  5. The Verification Game for $\forall^*\exists^*$
  6. Game-Based Verification Beyond $\forall^*\exists^*$
  7. Multiplayer Games and Partial Information
  8. HyperLTL Verification as an MPG$_\mathit{ii}$
  9. Soundness
  10. Hierarchical Information
  11. Completeness for $\exists^*\forall^*$
  12. Prophecy Variables
  13. Prophecies and Partial Information
  14. Prophecies and Prophecy Variables
  15. Prophecies and Games
  16. ...and 6 more sections

Key Result

lemma 1

For every LTL formula $\psi$, we can effectively construct a DPA $\mathcal{A}_\psi = (2^\mathit{AP}, Q_\psi, q_{0, \psi}, \delta_\psi,c_\psi)$ such that $\mathcal{L}(\mathcal{A}_\psi) = \{ t \in (2^\mathit{AP})^\omega \mid t \models_\mathit{LTL} \psi \}$.

Figures (1)

  • Figure 1: Simple Kripke structure over $\mathit{AP} = \{a\}$

Theorems & Definitions (28)

  • lemma 1: EsparzaKRS17Piterman07
  • definition 1: $\mathcal{G}^{\forall\exists}_{\mathcal{K}, \varphi}$,BeutnerF22
  • lemma 2: BeutnerF22
  • remark 1
  • example 1
  • definition 2: $\mathcal{G}_{\mathcal{K}, \varphi}$
  • theorem 1
  • example 2
  • lemma 3
  • lemma 4
  • ...and 18 more