0 votes

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? 
in * TF "Emb. Sys. and Rob." by (1.4k points)

1 Answer

+1 vote
 
Best answer

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 (91.8k 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

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
asked Jan 23 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
asked Feb 6 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
Imprint | Privacy Policy
...