Re: [tlaplus] Derivation of SF_vars(A) Strong Fairness

On Wednesday, October 25, 2023 at 5:57:32 AM UTC-7 Stephan Merz wrote:

All of these transformations are just tautologies of temporal logic and independent of fairness.
Concerning strong fairness: I'll write F for ENABLED <<A>>_v and G for <<A>>_v.

(1) => (3):

[]([]<>F => <>G)
=> [][]<>F => []<>G by the temporal logic rule [](A => B) => ([]A => []B)
=> []<>F => []<>G since [][]A <=> []A

(3) => (1): I'll reason semantically because it looks simpler.

Assume that a behavior sigma satisfies (3), i.e. []<>F => []<>G.
We need to show that sigma also satisfies []([]<>F => <>G).
So assume that there is some suffix tau of sigma for which []<>F is true, we need to show that tau satisfies <>G.
Since []<>F is true for tau, it is also true (a fortiori) for sigma, and by (3) we obtain that []<>G is true for sigma.
Therefore <>G is true for tau.

The equivalence of (2) and (3) is simply a consequence of the equivalence of F => G and ~F \/ G, plus of pushing negation across temporal operators (~[]F <=> <>~F, ~<>F <=> []~F).

Stephan

On 25 Oct 2023, at 00:52, Chris Ortiz <zitro...@xxxxxxxxx> wrote:

Hello,

I am trying to get a set of similar form of formulas between WF_vars(A) and SF_vars(A). In Specifying System book there are 3 formulas for WF_vars(A) which were derived by set of tautologies, namely:

Weak Fairness in Specifying System:
1) []([]ENABLED <<A>>_v => <><<A>>_v) <--- I called always the case imply form
2) []<>(~ENABLED <<A>>_v) \/ []<><<A>>_v <--- I called disabled OR form
3) <>[](~ENABLED <<A>>_v) => []<><<A>>_v <-- I called infinitely often action imply form

Strong Fairness in Specifying System:
2) <>[](~ENABLED <<A>>_v) \/ []<><<A>>_v <-- I called disabled OR form
3) []<>ENABLED <<A>>_v => []<><<A>>_v <-- I called infinitely often action imply form

I was searching for the "1) I called always the case imply form" of Strong Fairness and I stumble upon Ron Pressler's informative link: https://pron.github.io/posts/tlaplus_part3

Strong Fairness from Ron Pressler's link:
1) []([]<>ENABLED <<A>>_v => <><<A>>_v) <-- which I called always the case imply form. The one I am searching for.

What I am then trying to do is find the derivation of this 1) with the other 2) and 3) of Strong Fairness by method of tautologies just like in the Specifying System book. I am having a hard time with my logic.

I appreciate if you can help me with the derivation of equivalence for that Strong Fairness formulas.

Thanks,
Zitro

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/bf96558c-ca17-4bc5-b551-d9b641d1c655n%40googlegroups.com.