Translation to CTL

Question

I solved it like below :

If G!a is true then it means FGa is true hence overall result is true, if G!a is false then overall result is false because of AND. so It is reduced to AG!a

Q1. Is above solution correct ?

Q2. In the exam solution in the last step, A is moved inside the bracket, when can we just move outer A or E to inside. Could you please explain the rule regarding this ?

Answer 1

Your solution is not correct, you may argue as follows as shown in the example solutions:

        [!a WU false] & F[a WU b]
    <-> (G !a) & F[a WU b]
    <-> (G !a) & (F G a | F b)
    <-> (G !a) & (F b)

You cannot drop the Fb, and moving in the A-quantifier to the two temporal operators is also to be done finally to get the example sulution).

Q2: A distributes over conjunctions and E distributes over disjunctions.

Comments

Yes now I got it, I misinterpret it earlier.
Thanks for the clarification :)