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): fPQstate' FF-A FT-B TFFA TFTB TTFimpossible TTTB The interesting bit is the second-to-last ro...
