Translation of logics

Question

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. 

Answer 1

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?

Comments

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!