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

868 questions

986 answers


438 users

0 votes

According to this sample solution the property does not hold, but my solution shows it holds. 


So what could be the mistake in my solution? 

in * TF "Emb. Sys. and Rob." by (370 points)

1 Answer

0 votes
Best answer

You continued in s5 with the diamond operator, but that one has been removed by the rule before. Instead, it should have been a box operator there. And then, the property must also be shown in the other successor states of s5, but it does not hold in state s0:

by (139k points)
selected by
Why haven't we taken s4 as the successor of s5 instead of s0?
We have to check all the successors of s5, and started with s0. Since that already failed, there was no reason to continue with the other successor states.
So if box operator is there we have to check for all the successors and if there would be a diamond operator (just for assumption) we can check just one successor?
Right, that is explained  in detail on the slides and in the video.
Thank you, i got it now
Imprint | Privacy Policy