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

1.1k questions

1.2k answers


538 users

0 votes

I did not get the explanation at all. Is it ok if i simply write that it does not hold because of no path on s8 onwards, and mention CTL formula? 

in * TF "Emb. Sys. and Rob." by (440 points)
edited by
Did you post the wrong figure which is not related to your question?
Sorry, my picture was wrong previously. Now I have upodated it.

1 Answer

0 votes
No that would not be okay. We need to explain why A[c WU b] does not hold on all initial states, i.e., on state s3 and s6. We can explain that it does hold on s6 as follows: A[c WU b] is equivalent to b | c &AX A[c WU b], and since s6 satisfies b, it also satisfies A[c WU b].

However, it does not hold on s3, since on s3, we have c, but not b, so that we have to check that all successor states of s3, i.e., s5 satisfies A[c WU b]. This is however not the case, since s5 is neither labeled with b nor with c.
by (166k points)
Imprint | Privacy Policy