Prove properties of the form [](P => []P) with TLAPS

[Quentin DELAMEA]

Hello everyone,

I am new to TLAPS and am trying to prove the properties of a basic spec I wrote. One of the properties is of the following form:
\A x \in S: [](P(x) => []P'(x))

I found an example of a proof for a similar property in the AsyncTerminationDetection_proof.tla module for the Quiescence property in the Examples repository.

Here is the proof that is provided:

THEOREM Stability == Init /\ [][Next]_vars => Quiescence
<1>. TypeOK /\ terminated /\ [Next]_vars => terminated'
    BY DEF TypeOK, terminated, Next, DetectTermination, Terminate, RcvMsg, SendMsg, vars
<1>. QED  BY TypeCorrect, PTL DEF Quiescence

I admit that I don't understand this proof and would like to have more details so that I can adapt it to my case. Also, how do I handle the case where property P depends on x?

The property I am trying to prove is:

\A t \in TaskId: [](t \in FinalizedTask => [](t \in FinalizedTask))

where TaskId is a constant set and FinalizedTask is a set that can evolve with the next-state action.

Thank you for your help,

Quentin

[Andrew Helwer]

Minor point but formulas like [](P') are not - in general - stuttering insensitive. A formula F is stuttering insensitive if, for all possible behaviors, F satisfies a behavior if and only if F satisfies the same behavior with stuttering steps arbitrarily added or removed. All TLA+ formulas are supposed to be stuttering insensitive, but we currently don't have a fully-functional stuttering sensitivity checker. All of this is to say that the canonical stuttering-sensitive way to write your property would be [][\A t \in TaskId: t \in FinalizedTask => t' \in FinalizedTask]_vars, where [P]_v is a shorthand for P \/ UNCHANGED v. This is a bit easier to reason about than your formula and proving it should resemble an ordinary inductive proof of any [] property.

Andrew

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/a6b6effd-2e5b-42ec-96e6-91f47b4efdadn%40googlegroups.com.

[Andrew Helwer]

I will note that I'm pretty sure the formula [](\A t \in TaskId: t \in FinalizedTask => t' \in FinalizedTask) is coincidentally stuttering insensitive even when not boxed, simply because it states that something does not change and things do not change in stuttering steps. Still, it is a good habit to box properties involving primed variables.

[Andrew Helwer]

Correction: the formula should be [][\A t \in TaskId: t \in FinalizedTask => t \in FinalizedTask']_vars because FinalizedTask is the variable.

[Quentin DELAMEA]

Hi Andrew,

Thank you for response. I made a mistake when typing the message that changes its entire meaning. There is no prime on P.

I am interested in the properties of the form:
[](P => []P) and \A x \in S: [](P(x) => []P(x))

It seems to me that these formulas are valid (insensitive to stuttering).

Quentin

[Andrew Helwer]

You are correct those formulas are stuttering insensitive. It still might be easier to prove the [][\A t \in TaskId: t \in FinalizedTask => t \in FinalizedTask']_vars formula, though. It implies your intended formula, and can also be easily analyzed at the level of a single step. Here is a derivation:

WTS [][P => P']_v => [](P => []P):

Some theorems:

(a) [][]P = []P

(b) [](P => Q) => ([]P => []Q)

(c) []P => P

(d) (P /\ []P') => []P

[][P => P']_v [intro start]

[](P => P' \/ v' = v) [by definition of [P]_v]

[]((~P /\ P') \/ (~P /\ ~P') \/ (P /\ P') \/ v' = v) [long expansion of =>]

[]((~P /\ P') \/ (~P /\ ~P') \/ (P /\ P') \/ P = P') [P = P' if variables are unchanged]

[]((~P /\ P') \/ (~P /\ ~P') \/ (P /\ P') \/ (P /\ P') \/ (~P /\ ~P')) [expanding = for boolean predicates]

[]((~P /\ P') \/ (~P /\ ~P') \/  (P /\ P')) [dropping duplicate (P /\ P') and (~P /\ ~P')]

[](P => P') [contracting definition of =>; we've incidentally shown here our starting formula is stuttering-insensitive]

[][](P => P') [by theorem (a)]

[]([]P => []P') [implication by theorem (b)]

[](P => []P') [implication by theorem (c)]

[](~P \/ (P /\ []P')) [expanding definition of =>]

[](~P \/ []P) [implication by theorem (d)]

[](P => []P) [contracting definition of =>; goal reached!]

Andrew

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/00c1252f-6b80-499d-8f8f-dfb434d3f07an%40googlegroups.com.

[Stephan Merz]

Your property expresses that a condition P is stable, i.e. once it is true, it remains true forever. The standard way to prove this is to show

Inv => (P /\ [Next]_vars => P’)    or equivalently   Inv /\ P /\ [Next]_vars => P'

for a suitable invariant Inv (we are only interested in stability for all reachable states, the invariant serves to characterize those). The conclusion

[]Inv /\ [][Next]_vars => [](P => []P)

follows by simple (propositional) temporal logic. This is exactly what the quiescence proof in the example does (where TypeOK plays the role of the invariant).

As you say, your case is a little more complicated because P is not purely propositional but a first-order predicate with a parameter x. However, that parameter is bound outside the temporal-logic formula, so we can introduce a fresh parameter in the context and then pretend that P has no free variable anymore. (In the PM, we call this technique ``coalescing’’, you can find a pretty technical description of it at [1].)

Your proof should then look somewhat like this:

THEOREM Spec => \A t \in TaskId : [](t \in FinalizedTask => [](t \in FinalizedTask))

<1>. SUFFICES 

           ASSUME NEW t \in TaskId

           PROVE  Spec => [](t \in FinalizedTask => [](t \in FinalizedTask))

  OBVIOUS

<1>1. Inv /\ t \in FinalizedTask /\ [Next]_vars => (t \in FinalizedTask)’

   \* here you prove a non-temporal property 

<1>2. QED

  BY <1>1, Invariant, PTL DEF Spec

In the justification of the QED step, "Invariant" refers to a previously proved theorem Spec => []Inv. The definition of Spec must be used in order to relate the formula Spec to [Next]_vars, which appears in <1>1.

If you have trouble making this work, feel free to contact me off-list.

Hope this helps,

Stephan

[1] https://members.loria.fr/SMerz/papers/arqnl2014.html

[Quentin DELAMEA]

Thank you very much for your answers.

The process is now much clearer to me. I have managed to write the complete proof of my property. My first attempt was similar to the proof sketch proposed by Stephan, but I clumsily used the property name instead of the formula, which changed the meaning of the SUFFICES step leading to my error.

Now I understand much better why this proof works. I have one last quick question to make sure I have understood correctly. The invariant used in the proof allows us to characterize the states we are interested in for stability. If I understand correctly, this means that we can use any inductive invariant?

Quentin

[Stephan Merz]

Yes, any (inductive) invariant that is sufficiently strong to make the preservation of the stability predicate provable will do.

Stephan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/cb5d2fb9-0803-490a-bb5f-20257ebe3b8an%40googlegroups.com.

[Quentin DELAMEA]

Understood, thank you very much!