Hyperproperties

from blog Computer Things, | ↗ original
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...