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

On Thursday, November 27, 2025 at 10:47:10 AM UTC+1 Stephan Merz wrote:

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

Stephan

On 27 Nov 2025, at 10:44, Quentin DELAMEA <qdel...@xxxxxxxxx> wrote:

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
On Thursday, November 27, 2025 at 8:44:56 AM UTC+1 Stephan Merz wrote:
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

On 26 Nov 2025, at 21:41, Quentin DELAMEA <qdel...@xxxxxxxxx> wrote:

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

--
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...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/a6b6effd-2e5b-42ec-96e6-91f47b4efdadn%40googlegroups.com.

--
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...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/cb5d2fb9-0803-490a-bb5f-20257ebe3b8an%40googlegroups.com.