# Exam 2018 9.d

Hi,

How does the final answer satisfy EGFa? We can write the final answer as EFEGb However this does not satisfy EGFa which is a valid condition of the formula. Also Can we write EGFa = EGEFa ? edited

+1 vote

The last line (the one that does not start with an equal sign) is not equivalent to the previous ones as it omits EGFa which covered the previously mentioned case 2.

by (25.2k points)
selected by
Thanks for the answer, do you mean to say that the final answer is wrong? don't we have to write CTL formulas which are equivalent to the question?
I mean to say that the last line cannot be considered a correct final answer to the question.
Got it Thanks!
One more thing how is !(AFG !a) is a CTL formula? referring to 9.e part of 2018.08.21 ?
¬(AFG ¬a) itself is not a CTL but a CTL* formula as its quantifier G occurs without being E or A.
¬(AFG ¬a) is equivalent to EGF a. So there is a “not” missing in the text of 9a formula 5. And the correct class would be CTL* without LTL and CTL.
but in the solution it is claimed that its an CTL formula, I should assume that's wrong?
Yes. The correct class is CTL* without LTL and CTL (S4).
Thanks once again
For this formula, it is important to understand that if Fa holds at some point t1, then it also holds at any previous point t<=t1. If we have to make sure that Fa holds until b holds, then it must also hold at least right before the point of time where b holds. If b should hold already at the initial point of time, then that is also fine.

Hence, find that [F a SU b] <-> b | F((X b) & (F a)) is valid. Since we can express the WU by SU, we also get [F a WU b] <-> [F a SU b] | G F a, and thus, we have

[F a WU b] <-> b | F((X b) & (F a)) | G F a

We can still modify the formula a bit in that we replace F a with a | X F a and multiply out:

[F a WU b] <-> b | F(a & X b) | F X(b & F a) | G F a

Okay, what all that? Because now, we can drive in an outermost E-quantifier and will get the following formula:

E[F a WU b] <-> b | EF(a & EX b) | EF EX(b & EF a) | EGF a

This formula is almost a CTL* formula, it is just the expression EGFa which is not expressible in CTL. That it is sign that the entire formula may not be expressible in CTL, and indeed, this is the case: Note that for the special case of b=false, we get

E[F a WU false] <-> EGF a

and since EGFa cannot be expressed in CTL, it is also not possible to express E[F a WU b] (assuming that we could would lead to a contradiction).

Hence, the CTL formula given above must be definitely incorrect, since E[F a WU b] cannot be expressed in CTL.

That is different with a SU: Looking at the above transformations, we get

[F a SU b] <-> b | F(a & X b) | F X(b & F a)

and thus, we get the following CTL formula

E[F a SU b] <-> b | EF(a & EX b) | EF EX(b & EF a)
by (117k points)