Determining which states in a transition system satisfy a specific CTL formula [closed]
-
02-11-2019 - |
Question
Trying to answer the following question:
However, my answer is that only one of these states satisfy the TS (which is for sure wrong since the next part of this question asks to remove states that don't satisfy the formula and compute the new TS).
Reasoning follows:
1 - does not satisfy the formula since if you go to 4, EXISTS NEXT c is violated
2 - does not satisfy the formula since if you go to 4, EXISTS NEXT c is violated
3 - does not satisfy the formula since if you go to 1, EXISTS NEXT c is violated
4 - satisfies the formula since all paths satisfy EXISTS NEXT c
5 - does not satisfy the formula since if you go to 6, EXISTS NEXT c is violated
6 - does not satisfy the formula since if you go to 4, EXISTS NEXT c is violated
Can anyone see where I have gone wrong with my reasoning?
Something else I'm not sure about is for example if we take 4, it is satisfied since all paths lead to other states that (together) satisfy the equation. Do we need to include these 'other states' in the satisfaction set?
Really grateful for any help.
No correct solution