CTL Model Checking 1 (exercise sheet 9 question 1)

Question

S1=E G (a|b)

my solution: {s2}

S2=A G (a&b)

my solution: {s2}

S3=E F (b)

my solution: {s0,s2,s3,s4,s5,s6,s7}

S4=A F (a)

my solution: {s2}

all of my solutions are wrong and I don't know why! in page 13 of the solution file, is mentioned that when we can't satisfy a condition because of a deadend, we write that deadend as the final answer. So that's why I wrote {s2}.

Comments

Why don't you use the teaching tool to double-check your solution? It is not that I want you to use the teaching tool to create the solution that you will submit, but that the teaching tool can tell you whether your solution is right or wrong. Also, you can see how it has been computed in that case, and that could give you the clue on how to solve it correctly. Have a look at it!

---

you're right. the tool is good. but the problem is that I need someone to explain the concept to me in an easy language. using the tool, I don't understand what it did and how it came to the result. but when I ask my questions here and you tutors explain it to me, I understand really good :)

---

You are welcome! I don't want to stop you asking questions. If you need help, we are willing to help you, there should be no doubt about that. I just wanted to point out that for this particular exercise, the tool gives quite detailed "explanations". If you need more, don't hesitate to ask.

Answer 1

1. S1 = E G (a | b). Where do we have a | b? Certainly in all states except for s3, s1. Now whee can we form a loop that only uses states other than s3, s1? Since s2 has no successors, it also doesn't have any path and hence no path satisfying the criterion.
2. None of the states satisfy both a and b. Hence, we cannot form a loop of such states. But s1, s2 have no successors, hence no infinite paths, thus all of their paths satisfy any criterion. So you were correct about a2 but that weren't all states yet.
3. Since that's and existential formula, the states satisfying it need to have infinite paths. That excludes the deadends. Thus, s2 shouldn't be in the answer.
4. Similar to S2, you have to include all deadends (no successor means no infinite paths, no infinite paths means all (of the non-existent) infinite paths satisfy any criterion. Also, there is one more state from where all paths go through a states satisfying a.

This answer has been created by all of your tutors together in a meeting. ♥