Re: [tlaplus] Nondeterminism and equivalence

[Stephan Merz <stepha...@xxxxxxxxx>]

Safety properties constrain finite sequences of states (prefixes of behaviors), and the possibility of stuttering forever from any point – rather than actual stuttering invariance – effectively lets you represent finite sequences in an LTL framework. In standard LTL or with "raw TLA" specifications (where []A is a temporal formula for an arbitrary action A), the mere fact that the semantics talks about infinite sequences already introduces an element of liveness because "the clock ticks infinitely often". For example, the specification

   x = 0 /\ [](x' = x+1)

implies the liveness property

  \A n \in Nat : <>(x > n)

so the specification is not a safety property. The formula

  x = 0 /\ [](x' = x+1 \/ \E z : [](x=z))

is not stuttering invariant, but it still describes a safety property.

Stephan


> On 19 Nov 2016, at 23:19, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:
> 
> 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