On Sunday, November 20, 2016 at 1:59:54 PM UTC-8, Ron Pressler wrote:
On Sunday, November 20, 2016 at 2:38:23 PM UTC+2, Ioannis Filippidis wrote:
On the other hand, it could imply a liveness property
that doesn't mention steps (of the form `[]<> P` for `P` a state predicate).
Do you have an example of `Init /\ [][A]_v` implying `[]<> P` but not `[]P`?
Good point, no I do not have such an example. I think that the following claim can be proved.
(Please correct me if wrong.)
ASSUME:
1. VARIABLE v (* If there are more, define `v` as a tuple of all mentioned variables. *)
2. STATE Init(v), P(v)
3. ACTION A(v) (* The _expression_ `v'` can appear within the formula `A(v)`. *)
4. \EE v: Init(v)
5. No variable symbols other than `v` occur in `Init(v), P(v), A(v)`
6. |= ( Init(v) /\ [][ A(v) ]_v ) => ( []<>P(v) /\ ~ []P(v) )
PROVE: FALSE (* contradiction *)
Proof sketch:
<1>1. |= ([]<> P(v) /\ ~ [] P(v)) => (<>P(v) /\ <> ~P(v))
<2>1. |= []<> P /\ ~ []P \equiv []<> P /\ <> ~P
<2>2. |= []<> P /\ <> ~P => <> P /\ <> ~P
<2>3. QED. BY <2>1, <2>2.
<1>2. F == Init(v) /\ [][ A(v) ]_v
<1>3. \E sigma: IsABehavior(sigma) /\ sigma |= Init(v) (* So we can start from state `sigma[0]`. *)
<2>1. \EE v: Init(v) BY A3.
<2>2. QED. BY <2>1, DEF \EE, /\-elim.
<1>4. PICK sigma: IsABehavior(sigma) /\ sigma |= Init(v)
BY <1>3.
<1>5. tau == [n \in Nat |-> sigma[0] ]
<1>6. IsABehavior(tau) /\ tau |= F (* The behavior `tau` stutters forever at state `sigma[0]`. *)
<2>1. IsABehavior(tau) BY <1>4, <1>5, DEF IsABehavior.
<2>2. tau |= Init(v) BY <2>1, <1>4.
<2>3. tau |= [][ FALSE ]_v BY <2>1 (\A n \in Nat: tau[n] = tau[n + 1]).
<2>4. QED. BY <2>2, <2>3, TLA+ semantics.
<1>7. CASE sigma[0] |= P(v)
<2>1. tau |= [] P(v) BY <1>5, <1>7/A. (* A = Assumption *)
<2>2. tau |= ~ <> ~ P(v) BY <2>1.
<2>3. IsABehavior(tau) /\ tau |= F /\ ~ <> ~ P(v) BY <1>6, <2>2.
<2>4. QED. BY <2>3, <1>1, <1>2, A6.
<1>8. CASE sigma[0] |= ~ P(v)
PROOF: similar to that of <1>7.
<1>9. QED.
BY <1>7, <1>8, which are exhaustive.
So, the liveness property `[]<>P /\ ~ []P` requires that a nonstuttering step `<< sigma[k], sigma[k + 1] >>, k \in Nat` with
`sigma[k] |= P \equiv ~ sigma[k + 1] |= P` should eventually happen, and so cannot be implied by a formula of
the form `Init /\ [][A]_v`, for the same reason that a liveness property of the form `<><< B >>_v` cannot be implied.
I think that the comment about an example that does not imply `[]P` was a good observation that
suggests the following about the element of liveness
(which seems to be the main point about the clock "ticking" in the original comment):
a raw TLA safety property (e.g., `Init /\ []A`) can require liveness properties over nonstuttering steps,
whereas a TLA safety property (e.g., `Init /\ [][A]_v`) cannot.
ioannis