Hyperproperties • Buttondown

I wrote about hyperproperties on my blog four years ago, but now an intriguing client problem got me thinking about them again.1

We're using TLA+ to model a system that starts in state A, and under certain complicated conditions P, transitions to state B. They also had a flag f that, when set, used a different complicated condition Q to check the transitions. As a quick decision table (from state A):

The interesting bit is the second-to-last row: Q has to be strictly more permissible than P. The client wanted to verify the property that "the system more aggressively transitions when f is set", ie there is no case where the machine transitions only if f is false.

Regular system properties are specified over states in a single sequence of states (behaviors). Hyperproperties can hold over sets of sequences of states. Here the hyperproperties are:

That's pretty convoluted, which is par for the course with hyperproperties! It makes a little more sense if you have all of the domain knowledge and specifics.

Leave a Comment