Derivation of SF_vars(A) Strong Fairness

[Chris Ortiz]

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

[Stephan Merz]

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

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

[Chris Ortiz]

Hi Stephan,

Thank you very much. That is exactly the kind of explanation I am looking for. It is so satisfying for me to now have such reasoning about that specific Strong Fairness formula.

Best regards,

Zitro