Can I simplify the specification for global and local model checking?

Question

In the exam solution: https://es.cs.uni-kl.de/teaching/vrs/exams/2019.08.27.vrs/2019.08.27.vrs.solutions.pdf

problem 4a

But can I do this:

=E[a SU b]

=F[a SU b] ------(as EF=E or F)

=Fb ---------------(as F[a SU b]=Fb)

=AFb ------------(as AF=F)

= mu x. b V []x ---------------(As  AFa=mu x. a V []x)

then do local model checking? like this-

Answer 1

Fist of all, no E[a SU b] is not (E)F[a SU b]. You cannot just replace E by EF.

Second of all: No, the simplifications would for example also simplify the graph of the local model checking. Thus, we couldn't see whether you can handle the features we wanted to be there.

Answer 2

In general, you can simplify formulas, of course. However, your above simplifications don't make sense to me. E[a SU b] is not the same as F[a SU b], and Fb is not the same as AFb.