This concept deserves its own “entry”.
Hyperproperty definition
A hyperproperty is a set of a set of traces.[1]
Intuition
While trace properties are about runs in a single universe, hyperproperties can talk about “parallel universes”. A good example is fairness: you lost the lottery, but you could have won it.[1:1] While the paradigmatic example is noninterference, there is an application of them that I find interesting, namely a less crude way to replace liveness properties (which are really hard to ensure) by a more strict property.
The example is responsiveness, i.e., every request will eventually be served. This is a liveness property. Often one is finding a natural bound for how long it may take to get a response. Now, if we combine the idea with fairness, one could require that the system is fair and that for each run, there is an equivalent run such that requests are answered in time.
Why this post?!
I felt I should follow up with an explanation of a previous cryptic post of mine. And there, we shall need hyperproperties (besides that they are what information flow is typically about).
See more in this paper on how to enforce hyperproperties. ↩︎ ↩︎