The TOPLAS paper describes the temporal logic TLA,
And by the way : what has been added by Leslie Lamport to what had been discovered by Pnuelli?
The actions I guess: a certain way of combining primed and unprimed flexible variables.
But how could Pnuelli manage an algorithm without them?
--
FL