Question about importance of "⊨ F⇒ G implies ⊨ □F ⇒□G"

[Andrew Helwer]

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

[Hillel Wayne]

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

H

--
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/aea18811-d080-43b3-9497-63881aada9dbn%40googlegroups.com.

[Andrew Helwer]

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

[Stephan Merz]

Also think of refinement: infer [][LowNext]_lv => [][HighNext]_hv from [LowNext]_lv => [HighNext]_hv. In practice, we generalize a bit and infer []Inv /\ [][LowNext]_lv => [][HighNext]_hv from Inv /\ [LowNext]_lv => [HighNext]_hv, but this essentially just combines the basic rule with the fact that [](A /\ B) <=> []A /\ []B.

And in general, that rule underlies a lot of "simple temporal reasoning".

Stephan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/9ab8a317-61cb-49cf-b602-78f8bfde08ban%40googlegroups.com.

[divyanshu ranjan]

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 Mon, Dec 2, 2024 at 7:36 PM Stephan Merz <stepha...@gmail.com> wrote:

Also think of refinement: infer [][LowNext]_lv => [][HighNext]_hv from [LowNext]_lv => [HighNext]_hv. In practice, we generalize a bit and infer []Inv /\ [][LowNext]_lv => [][HighNext]_hv from Inv /\ [LowNext]_lv => [HighNext]_hv, but this essentially just combines the basic rule with the fact that [](A /\ B) <=> []A /\ []B.

And in general, that rule underlies a lot of "simple temporal reasoning".

Stephan

On 2 Dec 2024, at 14:52, Andrew Helwer <andrew...@gmail.com> wrote:

--
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/08616DEF-ACE0-42DA-8DC3-3753448405F8%40gmail.com.

[divyanshu ranjan]

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