# Translation of logics

Hi,

Translate E([a U b] ^ ¬ [c U d]) to CTL [2022.09.06 VRS].

Solution is given as

My approach is little bit different and I want to check the correct of this solution,

E([a SU b] & ¬ [c SU d]) =

= EF([a SU b] & ¬ [c SU d]) used E = EF

= EF(AG[a SU b] & AG[!c WB d]) used ![c SU d] = [!c WB d] and AG ->                                                                                                                                   vanishes,

= EF(AGA[a SU b] & AGA[!c WB d]) used AG = AGA

Can we use Vanishes gives AG , since AG can be entirely removed? Does that make valid CTL?   EF(AGA[a SU b] & AGA[!c WB d]) is a valid CTL as per my understanding.

No, that is not correct. E is not equivalent to EF, so the first step is already incorrect. Also in the particular formula, the two formulas E([a SU b] & ¬[c SU d]) and EF([a SU b] & ¬ [c SU d]) are not equivalent.

Second, where do the AG operators in the second step come from?
by (166k points)
There is a formula in the cheat sheet, AG can be vanishes.  I thought, I can add AG to anywhere if Nothing is there.
AG -> Vanishes,
Vanishes->AG will it work in the reverse direction?
Which cheat sheet do you mean? AG cannot be simply added or removed. AG phi means that phi holds on all states reachable from a state s while phi just means that it holds on the current state s. That is a different formula!