Re: [tlaplus] Question about importance of "⊨ F⇒ G implies ⊨ □F ⇒□G"

[divyanshu ranjan <idivyanshu.ranjan@xxxxxxxxx>]

In https://lamport.azurewebsites.net/pubs/lamport-actions.pdf, Figure 5 mentions various rules of
Simple Temporal Logic, Basic and Additional Rules of TL.

Further is mentioned that The validity of TLA1–SF2 can be proved using STL1–STL6 and
the RTLA rule □P ≡ P ∧ □(P ⇒ P ′). It would be instructive to prove any of TLA1-SF2 and see

how rule STL4 is used (Rules TLA1-SF2 can be used to prove invariants, leads to proofs when

action is weakly fair and strongly fair etc).

When I tried to prove WF1 I reached out to STL4.

Using backward chain of reasoning

To prove □[N]_f ∧ WF_f (A) ⇒ (P ~> Q),
  I need to prove □([N]_f ∧ ([]Enabled <A>_f ⇒ ◇ <A>_f)) ⇒ (P ~> Q) (Rule STL5),

  I need to prove [N]_f ∧ ([]Enabled (A)_f ⇒ ◇ A_f)  ⇒ (P ⇒ ◇ Q) (Rule STL4) ...

Thanks

Divyanshu Ranjan

On Monday, December 2, 2024 at 7:22:39 PM UTC+5:30 Andrew Helwer wrote:

I think that would make sense. Since ⊨ F means F holds for all behaviors, not just those satisfying a given spec, if we look at the formula:

⊨ Next ⇒ Prop

Where both Next and Prop are anywhere from constant- to step-level formulas since we are using Raw Temporal Logic of Actions (RTLA) here (main difference is RTLA formulas are not required to be stuttering-invariant), then I guess rule (3.12) gives us a way to prove ⊨ □Next ⇒ □Prop without using induction. Also note that ⊨ Next ⇒ Prop holds for all behaviors, not just ones where the first step satisfies Next, because all behaviors with a first step not satisfying Next will make Next ⇒ Prop vacuously true.

I guess this means that if we prove Next ⇒ Prop without using induction, like just using symbolic manipulation without binding any of the spec variables - or equivalently, just proving Prop when considering behaviors with a first step satisfying Next - we will have proven ⊨ □Next ⇒ □Prop, and from there it's a short hop to the standard TLA spec formula ⊨ Init ∧□[Next]_vars ⇒ □Prop.

I'll re-read that section of the book since I think there is an example of such a non-inductive proof.

Andrew Helwer

On Sunday, December 1, 2024 at 9:49:42 PM UTC-5 Hillel Wayne wrote:

Could it be related to invariants? Next => Prop implies []Next => []Prop?

H

On 12/1/2024 3:06 PM, Andrew Helwer wrote:

On page 64 of A Science of Concurrent Programs we have the formula:

(3.21) ⊨ F⇒ G implies ⊨ □F ⇒□G

which Lamport claims "lies at the heart of much temporal logic reasoning."

I understand why the rule is true, but I have been wracking my brains trying to figure out how it is so fundamental and can't really come up with anything. Can anybody think of an example? Thanks!

Andrew Helwer

--
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/aea18811-d080-43b3-9497-63881aada9dbn%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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/eef0d22d-0e4a-4a8c-a46b-c1b620b6fb47n%40googlegroups.com.