HyperLTL

Origin. Clarkson, Finkbeiner, Koleini, Kuz, Rabe introduced HyperLTL (2014). Temporal logic for hyperproperties. Extends LTL with trace quantifiers. Express information flow, observational determinism. Model checking hyperproperties.

Models. LTL over multiple traces. LTL: properties of single infinite traces. HyperLTL: quantify over traces, relate them. ∀π∀π'. (aπ ↔ aπ') → (bπ ↔ bπ'): non-interference. Traces labeled, propositions indexed by trace variable.

Formalism.

Syntax: ψ ::= ∃π.ψ | ∀π.ψ | φ φ ::= aπ | ¬φ | φ ∧ φ | Xφ | φUφ

Trace variables: π, π', π₁, ... aπ: proposition a on trace π.

Semantics: Evaluated over trace assignment Π: Var → Traces. T, Π, i ⊨ aπ iff a ∈ Π(π)(i) T, Π, i ⊨ ∀π.ψ iff for all t ∈ T, T, Π[π↦t], i ⊨ ψ T, Π, i ⊨ ∃π.ψ iff for some t ∈ T, T, Π[π↦t], i ⊨ ψ

Example — observational determinism: ∀π∀π'. G(oπ ↔ oπ') → G(aπ ↔ aπ') "Same observations imply same actions."

Example — non-interference: ∀π∀π'. G(lowπ ↔ lowπ') → G(outπ ↔ outπ') "Same low inputs, same outputs."

Example — symmetry: ∀π∃π'. G(swapped(aπ, aπ')) "For every trace, there's a swapped version."

Fragments:

∀*: all universal (safety hyperproperties)
∃*: all existential (liveness)
Alternation increases complexity

Symbols.

Symbol	Unicode	Name	Meaning
∀π	—	For all traces	Universal
∃π	—	Exists trace	Existential
aπ	—	Prop on trace	Indexed proposition
G	—	Globally	Always
F	—	Eventually	Finally
X	—	Next	Next step
U	—	Until	Until

Metatheory. Model checking: decidable but expensive. ∀* fragment: PSPACE in formula, NLOGSPACE in system (like LTL). Alternation: exponential blowup per alternation. Satisfiability: undecidable for ∀∃. ∀* and ∃* fragments decidable.

Applies to. Information flow security. Non-interference verification. Observational determinism. Privacy properties. Fault tolerance. Symmetry. Service level agreements.

Limitations. High complexity with alternation. Synthesis: very expensive. Infinite traces required. Tool support developing (MCHyper, etc.). Specification challenging. Counterexamples complex.