Hyperproperty¶
A system specification whose truth depends on the system's whole set of possible execution traces, allowing relations among multiple runs such as noninterference and observational determinism.
Core Idea¶
Let (Phi) be a universe of execution traces. An ordinary trace property is a set \(P\subseteq\Phi\): one trace either belongs or does not. A system is represented by its set of possible traces \(S\subseteq\Phi\). A hyperproperty is a set of such systems,
so satisfaction asks whether \(S\in H\). This one-level lift lets a specification compare alternative executions. Noninterference, for example, says that runs differing only in secret inputs must agree in their public observations; no verdict on one trace can establish that relation.
Scope of Application¶
Hyperproperties formalize information-flow confidentiality and integrity, observational determinism, noninterference, declassification policies, symmetry, robustness, quantitative leakage bounds, and some service-level or data-minimization conditions. HyperLTL adds explicit trace quantifiers to temporal logic for finite-state reasoning.
Verification cost rises sharply with quantifier alternation and number of traces. Some subclasses reduce to ordinary safety on a self-composed product; general hyperproperty verification need not.
Clarity¶
State the trace alphabet, system semantics, trace quantifiers, observation relation, alignment convention, and whether nondeterminism is demonic, angelic, or merely enumerated. Give the minimal counterexample shape. Calling noninterference a “property of outputs” hides the essential comparison across runs.
Manages Complexity¶
The abstraction unifies policies once treated as unrelated exceptions to trace logic. It tells a verifier why a single counterexample trace is insufficient, how many traces a violation needs, and which proof transformation may work. The semantic type itself becomes a routing rule from specification to tool.
Abstract Reasoning¶
- Define the system's trace semantics.
- Ask whether the desired verdict can be determined trace by trace.
- If not, identify the required trace tuple or quantifier pattern.
- Express the condition as membership of the complete trace set.
- Classify it as hypersafety, hyperliveness, or a combination.
- Determine whether it is k-safety.
- Select self-composition, relational logic, or hyper-temporal model checking.
- Produce counterexample trace sets rather than isolated traces.
Knowledge Transfer¶
The portable pattern is raise the object of evaluation from one behavior to a population of possible behaviors so cross-instance relations become expressible. It transfers to algorithmic fairness across individuals, differential privacy across adjacent datasets, robustness across perturbations, and relational program equivalence. The proposed immediate parent is Constraint.
Relationships to Other Abstractions¶
Current abstraction Hyperproperty Domain-specific
Parents (1) — more general patterns this builds on
-
Hyperproperty is a kind of Constraint Prime
Constraint is the proposed immediate parent because a hyperproperty partitions trace-set systems into admissible and inadmissible ones.
Hierarchy path (1) — routes to 1 parentless root
- Hyperproperty → Constraint
Neighborhood in Abstraction Space¶
Hyperproperty sits in a sparse region of the domain-specific corpus (91st percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Unclustered & Miscellaneous (1565 abstractions)
Nearest neighbors
- Model Checking — 0.79
- Maximal set (computability theory) — 0.78
- Computation Tree Logic — 0.78
- Reduction (Computability Theory) — 0.78
- Formal Verification — 0.77
Computed from structural-signature embeddings · 2026-09-08