On Saturday, November 19, 2016 at 2:19:39 PM UTC-8, Ron Pressler wrote:
I haven't thought it through, but it seems to me that without stuttering invariance, machine specifications would still be safety properties (i.e., closed), but safety properties would be able to specify undesired "prescience". Stuttering pushes future events indefinitely ahead, into the realm of liveness properties, which makes prescience a machine-closure-breaking liveness property.
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.
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 [1].
[1] https://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#what-good
Ron
ioannis