Determining which states in a transition system satisfy a specific CTL formula [closed]

cs.stackexchange https://cs.stackexchange.com/questions/41882

  •  02-11-2019
  •  | 
  •  

Question

Trying to answer the following question:

enter image description here

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

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top