# Problem 8.Conversion 2019.08.27

Hi,

I have some issues regarding Conversion from CTL to LTL and vice versa.

• How is !AGAXAFb equivalent to EFEGEX !b?
• How is !AXXGF!E[1 SU (Ab)] =  EXXFGE[1 U (Ab)] shouldn't it be !EXXFGE[1 U (Ab)]?
• For Question A([!a WU 0] & F [a WU b]) , We can derive as an alternative CTL form as  ! EG !a &  !EFE[a WU b]. Is this acceptable as a solution or we have to simplify more?

+1 vote

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=EFEp```

and 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&Aq```

at 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&Aq```

The 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
```
by (162k points)
selected by
Thanks for the answer, for third part I am a bit confused by my solution what is did is as follows
A([!a WU 0] & F[a WU b])
A (something) =  !E (something)
!E ([!a WU 0] & F [a WU b])
F = EF and EF = EFE so we have

!E ([!a WU 0] & EFE [a WU b])
Which can be rewritten as

!E G ! a & !EFE [a WU b])
A (something) =  !E (something) is wrong, it should be A (something) =  !E! (something)
Got it thanks alot