[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 25 Oct 2023 14:57:16 +0200*References*: <bf96558c-ca17-4bc5-b551-d9b641d1c655n@googlegroups.com>

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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BF7136CB-531A-4117-991C-4D09C3F13E15%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Derivation of SF_vars(A) Strong Fairness***From:*Chris Ortiz

**References**:**[tlaplus] Derivation of SF_vars(A) Strong Fairness***From:*Chris Ortiz

- Prev by Date:
**Re: [tlaplus] Why vars is defined as tuples instead of set** - Next by Date:
**Re: [tlaplus] Derivation of SF_vars(A) Strong Fairness** - Previous by thread:
**[tlaplus] Derivation of SF_vars(A) Strong Fairness** - Next by thread:
**Re: [tlaplus] Derivation of SF_vars(A) Strong Fairness** - Index(es):