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

769 questions

886 answers

1.3k comments

424 users

0 votes

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 ?

in * TF "Emb. Sys. and Rob." by (1.4k points)
edited by

2 Answers

+1 vote
 
Best answer
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.

About the second part of the question: No, EGFa and EGEFa are different. See also: https://q2a.cs.uni-kl.de/2013/issues-regarding-ctl-ltl-w-automata
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
0 votes
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)

Related questions

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