On Sunday, November 20, 2016 at 1:03:42 AM UTC+2, Ioannis Filippidis wrote:
A small comment: outside TLA, a formula of the form `Init /\ [] SomeAction` can "block later", because some step other than the first few violates the formula.
Stuttering allows `Init /\ [][ SomeAction ]_v` (outside TLA: `Init /\ []( SomeAction \/ (v = v') )`)
to reach just before the state where it would have blocked above, and then remain there, stuttering forever (the `v = v'` term).
This infinite stuttering may still be undesired, and a liveness property can require that it doesn't happen.
That is precisely the "painting into a corner" that Dederichs and Weber
mention in the paper that Abadi, Lamport et al.
respond to. By delaying the point of hitting the wall indefinitely, stuttering invariance pushes any prescient behavior that avoids it into a (machine closure breaking) liveness property. But while D&W try to redefine liveness so that it never breaks machine closure, A&L respond that non-machine closed specifications are useful for abstraction.
So far, I've seen invariance under stuttering justified as pragmatic or obvious, but this is an additional justification, it seems.
Stuttering invariance is also useful for comparing specifications at different levels of abstraction
Yes, that's the pragmatic justification I was referring to. The "obvious" one was that it hides internal behavior (the two are really just one).
Ron