Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes
Q. EF¬ [a B Gb]

EF[¬ a SU Gb]   

EGb  // F[a SU Gb] = Gb

Could you please let me know if this is correct ?
in * TF "Emb. Sys. and Rob." by (2.9k points)

1 Answer

+1 vote
 
Best answer

Almost, I think, there are these two ways to generate a CTL formula

    EF¬[a WB Gb] = EF[¬a SU Gb] = EF E[¬a SU Gb] = EF E[¬a SU EGb]

or

    EF¬[a WB Gb] = EF[¬a SU Gb] = EFGb = EF EGb

by (170k points)
selected by
Thank you for the explanation.

For the second part  
EF¬[a WB Gb] = EF[¬a SU Gb] = EFGb = EF EGb

In this you have replaced F[¬a SU Gb] to FGb, so does it mean F[¬a SU Gb] = FGb or you are seeing whole context of EF[¬a SU Gb] ?

I have read that F[¬a SU Gb] = Gb, could you please correct me ?
We have F[¬a SU G b] <-> F G b, but not F[¬a SU G b] <-> G b. Here is a little proof, but you may also use https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html to check:

F[¬a SU G b] = F(Gb | ¬a & X[¬a SU G b]) = FGb | F(¬a & X[¬a SU G b]) = FGb

The latter is seen as follows: if FGb holds, both FGb | F(¬a & X[¬a SU G b]) and  FGb are true. Otherwise, we have GF¬b, so that infinitely often b is false, and therefore Gb must be always false. But then [phi SU Gb] is also always false.
I got your point.
Thank you for the explanation.

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...