There are four temporal operators, and therefore we abbreviate these with the four state variables, and you may expect now also four fairness constraints. Indeed, we can add the following ones:
- GF(q0 | b) which stems from q0 := [a WB b]
- GF(q1 -> q0) which stems from q1 := F q0
- GF(c -> q2) which stems from q2 := G c
- GF(q3 -> a) which stems from q3 := [q2 SU a]
However, due to monotonicity of temporal operators, we do not need the fairness constraints for positive occurrences of weak temporal operators like G, WU, WB and negative occurrences of strong temporal operators like F, SU, SB, and therefore, the constraints for q0 := [a WB b] and q2 := G c are not required. It is not wrong adding anyone of them, but they are just redundant and not required. See slides 81-86 of the related chapter.
