Re: Nondeterminism and equivalence

[Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>]

P.S.

I was also surprised to learn how invariance under stuttering interacts with this issue. 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. So far, I've seen invariance under stuttering justified as pragmatic or obvious, but this is an additional justification, it seems.

Ron