[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Question about importance of "⊨ F⇒ G implies ⊨ □F ⇒□G"
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/9ab8a317-61cb-49cf-b602-78f8bfde08ban%40googlegroups.com.