Aside from WF and SF?

[Chris Ortiz]

Hello,

WF_v(A) == []([]ENABLED <<A>>_v => <><<A>>_v) and

SF_v(A) == []([]<>ENABLED <<A>>_v => <><<A>>_v)

Is there

[]( ENABLED <<A>>_v => <><<A>>_v) and

[](<>[]ENABLED <<A>>_v => <><<A>>_v ?

And what could they mean?

Thanks and best regards,

Chris (Zitro)

[Andrew Helwer]

[](ENABLED <<A>>_v => <><<A>>_v) is equivalent to []((ENABLED A) ~> <><<A>>_v) which means if an A step is enabled (like at all), eventually it will be taken; moreover, it will also be taken after every time an A step is enabled in the future. This is like an even stronger fairness assumption, but looking through the texts I have it does not seem to be a standard one. The usual next strongest fairness assumption in temporal logic is unconditional fairness, which is just []<><<A>>_v. There are a lot of fairness definitions out there though so I'm sure someone has covered & named it.

For the second one, since P => <>P, it seems to be implied by weak fairness. So it is at most as strong as weak fairness. Is it any weaker than weak fairness? I can't think of how it could be, but then we should be able to rewrite it into weak fairness. And there I am somewhat at a loss.

Andrew

--
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/98c4554e-2498-448c-86fd-ada5308a4c11n%40googlegroups.com.

[Stephan Merz]

As Andrew suspects, the second formula is equivalent to weak fairness:

THEOREM

ASSUME NEW ACTION A, NEW STATE v

PROVE WF_v(A) <=> [](<>[]ENABLED <<A>>_v => <><<A>>_v)

BY PTL

Stephan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUVG%2B-mRqwsUuRxDNGae_7PScdDf145WQ0T91yWFzSuQVA%40mail.gmail.com.

[Andrew Helwer]

Thanks, Stephan! Another interesting question that occurs to me is whether the first formula is equivalent to unconditional fairness, since presumably a step must be enabled before it can be taken. Thus the ENABLED A precondition seems redundant.

Andrew

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/47D2E34E-4119-41D3-8989-B4A296A3D5E1%40gmail.com.

[Stephan Merz]

[](ENABLED <<A>>_v => <><<A>>_v) is weaker than []<><<A>>_v. In particular, the former is true of a behavior in which <<A>>_v is never enabled. Neither of the two notions is "feasible" [1] (or machine closed) in the sense that any finite computation can be extended to a computation satisfying the fairness condition. Clearly, []<><<A>>_v cannot be made true if <<A>>_v is never enabled, and the same is true for 

XF_v(A) == [](ENABLED <<A>>_v => <><<A>>_v)

Suppose that you have two actions A and B that can be simultaneously enabled but where each one disables the other, then it may be impossible to ensure XF_v(A) /\ XF_v(B) for an execution.

In contrast, countable conjunctions of weak and strong fairness conditions are machine closed.

Stephan

[1] K.R. Apt, N. Francez, S. Katz: Appraising fairness in languages for distributed programming. Distributed Computing (1988), https://ir.cwi.nl/pub/10301/10301D.pdf

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUV5V-V%2BYuwpyAQmHuZKXaO23U8OUYN9uZTgKR4wU%2BXt4A%40mail.gmail.com.

[Chris Ortiz]

Thank you Andrew and Stephan. I was thinking the same way but I don't trust my intuition as I don't know how to formally prove it.

For the second formula.

[](<>[]ENABLED <<A>>_v => <><<A>>_v)

[]<>[]ENABLED <<A>>_v => []<><<A>>_v

<>[]ENABLED<<A>>_v => []<><<A>>_v

~<>[]ENABLED<<A>>_v \/ []<><<A>>_v

[]~[]ENABLED<<A>>_v \/ []<><<A>>_v

[](~[]ENABLED<<A>>_v \/ <><<A>>_v)

[]([]ENABLED<<A>>_v => <><<A>>_v) which is WF_v(A)

So it means the second formula is just a tautology of WF_v(A), or equivalent.

For the first formula

[](ENABLED <<A>>_v => <><<A>>_v)

[]ENABLED<<A>>_v => []<><<A>>_v

~[]ENABLED<<A>>_v \/ []<><<A>>_v <--- This is where I mind got short-circuited

As per Andrew, if this is unconditional fairness then this should be equivalent to []<><<A>>_v, for which I don't know how to derive.

Thanks and best regards,

Chris (Zitro)

[Chris Ortiz]

Hi Stephan,

Thank you. Do you mean never enabled (which I think is []~ENABLED) , or it should be not always enabled (which is ~[]ENABLED)?

Best regards,

Chris (Zitro)

[Andrew Helwer]

Thanks for the notes on the first formula, Stephan.

Ah, good derivation Chris! In my head I was thinking that [](P => Q) does not equal []P => []Q, because => is "disjunctive-y" (translates to ~P \/ Q) and [] only distributes over conjunction, not disjunction. But looking closely we can see:

1. [](P => Q)
2. [](~P \/ Q) [translating => into disjunctive form]
3. []~(P /\ ~Q) [De Morgan's law]
4. ~<>(P /\ ~Q) [rewriting []~ to ~<>]

Hmm, I actually get stuck here, since now we have the opposite situation where <> doesn't distribute over /\. Looking on page 64 of A Science of Concurrent Programs by Lamport he calls the tautology [](P => Q) => []P => []Q we are trying to prove "obvious". I can intuitively get why this is true but writing the derivation is not so obvious to me! Maybe I can try a different approach by reasoning over traces:

1. Consider all traces sigma satisfying [](P => Q); we want to prove each sigma also satisfies []P => []Q
2. Thus each state in each trace sigma satisfies either ~P (vacuous case) or P /\ Q
3. Consider the case where at least one state in sigma satisfies ~P:
1. In this case, the formula []P => []Q is vacuously true because []P is false
4. Consider the case where all states in sigma satisfy P /\ Q (i.e. no states satisfy ~P):
1. Thus each state satisfies P, and each state satisfies Q
2. Since each state satisfies P, sigma satisfies []P
3. Since each state satisfies Q, sigma satisfies []Q
4. Thus sigma satisfies []P => []Q in this case
5. QED: in all cases where sigma satisfies [](P => Q), it also satisfies []P => []Q

So using this method was mechanically easy. My mistake was thinking in terms of rewriting (equality), when really I had to think in terms of implication; [](P => Q) => ([]P => []Q), but the converse is not true! So I wonder how I could use this to write a simpler proof.

Andrew

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/f72d05f1-f38b-42d6-bed4-6d70e7989ddbn%40googlegroups.com.

[Stephan Merz]

I meant []~ENABLED. As soon as the action is enabled at some point, your condition requires <<A>>_v to eventually occur. 

Stephan

On 13 Nov 2025, at 19:18, Chris Ortiz <zitro...@gmail.com> wrote:

Hi Stephan,

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/292f0d2e-3021-44a3-b4e8-1df70431a53en%40googlegroups.com.

[Chris Ortiz]

Thank you Stephan. I really need to think it thru, I just can't get it reason out yet in my head. I was wondering if the first formula is weaker than []<><<A>>_v, is it stronger than SF_v(A)?

Hi Andrew, you are right....my derivation got short cut too much between = and =>. I am not sure if another derivation attempt of mine below makes sense or not.

[](<>[]P => <>Q)
[](<>[]P => <>Q) => ([]<>[]P => []<>Q)
                                     <>[]P => []<>Q
                              ~<>[]P \/ []<>Q
                                      []~[]P \/ []<>Q
[](~[]P \/ <>Q)  <=       []~[]P \/ []<>Q
[]([]P => <>Q)   <=>  WF
                            =    WF

[Andrew Helwer]

Yes, your first formula is stronger than strong fairness, because strong fairness requires an action must always eventually be enabled whereas in your first formula, it only needs to be enabled once. Consider a system where action A is enabled twice, then never again. If your first formula is asserted for action A, that means either the first or second time A is enabled it must be taken. This also explains why the first formula is not machine-closed, because your system has to "see the future" to know that A will never be enabled again, so it has to be taken the second time it is enabled.

For your derivation of the second formula, I don't follow the line [](~[]P \/ <>Q) <= []~[]P \/ []<>Q; could you explain?

Andrew

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/900092c4-d004-42fc-a049-5a1036877e1cn%40googlegroups.com.

[Chris Ortiz]

Thank you Andrew for explaining. 

That formula is a tautology of ([]F) \/ ([]G) => [](F \/ G).

Best regards,

Chris (Zitro)

[dbah...@gmail.com]

All,

 

I have been studying this hugely valuable work for a month or two now – and I am wondering about its status: on the opening page it suggests that you can provide error reporting – but there is no contact – and as far as I can see no way to contact the author – who is retired of course. Is this document to be maintained by the foundation? Or is it just what it is?

 

Is there any list of corrections?

 

Thanks

Dave Hughes