Most of the folloiwng is just generating of a NNF (see slides):
!AGAXAFb
= E!GAXAFb // since !Ap = E!p
= EF!AXAFb // since !Gp = F!p
= EFE!XAFb // since !Ap = E!p
= EFEX!AFb // since !Xp = X!p
= EFEXE!Fb // since !Ap = E!p
= EFEXEG!b // since !Fp = G!p
= EFEGEX!b // since EXEGp = EGEXp
The latter is easily seen by checking the semantics. Similar rules can applied to transform the other formula to CTL
!AXXGF!E[1 SU (Ab)]
= EXXFG!!E[1 SU (Ab)]
= EXXFGE[1 SU (Ab)] // since !!p=p
= EXXFGEFAb // since [1 SU p] = Fp
= EXEXEFEGEFAb // EXp = EXEp and EFp=EFEpand third
A([!a WU 0] & F [a WU b])
= A(G(!a) & F [a WU b]) // since [p WU 0] = Gp
= AG!a & AF[a WU b]) // since A(p&q) = Ap&Aqat that point you can pull out AG!a=!EFa, but that yields !EFa & AF[a WU b]), there is no negation on the second subformula AF[a WU b]). So, I don't see how you could come up with !EG!a & !EFE[a WU b] which would be equivalent to AFa & AGA[(!a) SB b] which is not the same.
AG!a & AF[a WU b]) is not yet CTL, and unfortunately AFp != AFAp in general. However, we can continue as follows:
:
= AG!a & AF([a SU b] | G a)) // since [a WU b] = [a SU b] | G a
= AG!a & A(F[a SU b] | F G a)) // since F(p|q) = F p | F q
= AG!a & A(F[a SU b] | F G a)) // since F(p|q) = F p | F q
= AG!a & A(F b | F G a)) // since F[a SU b] = F b
= AG!a & AF(b | G a)) // since F(p|q) = F p | F q
= A(G!a & F(b | G a)) // since Ap&Aq = A(p&q)Now, understand what the formulas says. G!a & .. means that on the paths, the variable "a" must always be false, so we may replace "a" by false in the remaining formula on the right hand side. Thus, we get
:
= A(G!a & F(b | G false)) // since G!a & p = G!a & (p[a<-false])
= A(G!a & F(b | false)) // since G false = false
= A(G!a & Fb) // since p|false = p
= AG!a & AFb // since A(p&q) = Ap&AqThe latter could have been done more efficiently as follows:
A([!a WU 0] & F [a WU b])
= A(G!a & F [a WU b])
= A(G!a & F [0 WU b])
= A(G!a & Fb)
= AG!a & AFb
