# Doubt in validity checking

For the above question, is the automata construction(below image) right ?

I know we can remove the first GF constraint(positive occurence of weak), but did not understand how we can remove the second one.
If we choose not to remove the second constraint what would be the accepting states out of ({},p,q,pq)
can someone please clarify this ?

As explained in the solution of the exam problem, the formula [a SU [b WU a]] is equivalent to [a WU [b WU a]] so that we can replace the SU operator in the formula by a WU operator to obtain the second equivalent formulation. If that one is translated, no fairness constraints are generated and we get the following automaton:

A({p,q},q,(p <-> a ⋁ b ⋀ Xp) & (q <-> p ⋁ a ⋀ Xq), true)

Why is that so? Note that [phi SU psi] and [phi WU psi] only differ in the case where G(phi&!psi) holds. In that case, [phi SU psi] is false and [phi WU psi] is true. Hence, the formulas [a SU [b WU a]] and [a WU [b WU a]] may only differ if G(a&![b WU a]) holds. The latter is however a contradiction: G(a&![b WU a]) is equivalent to (Ga)&(G![b WU a]), so we must have Ga to satisfy this formula. But then also [b WU a] always holds, and therefore ![b WU a] is always false. Thus, we cannot have (Ga)&(G![b WU a]), and therefore, we cannot have G(a&![b WU a]), and thus, [a SU [b WU a]] and [a WU [b WU a]] never differ!

Therefore, we translate the equivalent formula [a WU [b WU a]] to a safety automaton:

A({p,q},q,(p <-> a ⋁ b ⋀ Xp) & (q <-> p ⋁ a ⋀ Xq), true)

This automaton formula just requires that a word has an accepting run of infinite length.

If we translate the original formula [a SU [b WU a]], we would get

A({p,q},q,(p <-> a ⋁ b ⋀ Xp) & (q <-> p ⋁ a ⋀ Xq), GF(q->p))

In that case, a run is accepted, if it infinitely often satisfies q->p which is equivalent to p&q|p&!q|!p&!q. Thus, the set of the three states p&q, p&!q, !p&!q must be visited infinitely often, which means that at least one of these states must be visited infinitely often.
by (166k points)
Thank you so much.