HyperLTL

Origin. Clarkson, Finkbeiner, Koleini, Micinski, Rabe, and Sánchez introduced HyperLTL (POST 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
⊨	U+22A8	Satisfaction	Truth under a trace assignment at position i
Π	U+03A0	Pi (capital)	The trace assignment Var → Traces
π	U+03C0	Pi	A trace variable
↦	U+21A6	Maps to	Assignment update Π[π ↦ t]
↔	U+2194	Biconditional	Agreement of two traces on a proposition

Metatheory. HyperLTL is the trace-quantifier extension of LTL introduced by Clarkson, Finkbeiner, Koleini, Micinski, Rabe, and Sánchez (POST 2014) to give a specification language for the hyperproperties of Clarkson and Schneider (2010) — sets of sets of traces, which no property of individual traces can capture. Model checking against a finite Kripke structure is decidable by self-composition: the quantifier prefix is compiled into a product of the system with itself, one copy per trace variable, and the body is then checked as an LTL formula. This makes the alternation-free ∀* fragment PSPACE-complete in the formula and NLOGSPACE in the system, matching LTL, while each further quantifier alternation adds an exponential, so the complexity in the formula is non-elementary in the alternation depth. Satisfiability separates along the same seam: the ∃∀ fragment is decidable, and ∀∃ is already undecidable (Finkbeiner and Hahn, CONCUR 2016). Synthesis is undecidable beyond restricted fragments.

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

Limitations. Quantified traces are compared in lockstep, position against matching position, so hyperproperties whose traces must be aligned at different rates are not expressible and asynchronous variants had to be defined separately. The quantifier prefix is prenex: trace quantifiers cannot appear under temporal operators, which rules out properties requiring a fresh trace to be chosen at each step. Each formula relates a fixed finite number of traces, so no hyperproperty of unbounded arity can be stated. The body is an LTL formula, so the star-free ceiling survives — "p at every even position on π" is as unstatable here as in LTL. Alternation costs an exponential apiece, making the formula complexity non-elementary, ∀∃ satisfiability is undecidable, and there is no probabilistic reading, so quantitative information flow needs a different logic.