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

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.

## closed as unclear what you're asking by D.W.♦, David Richerby, Juho, Gaste, Luke MathiesonMay 2 '15 at 9:39

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

A hint that might put you in the right direction: Note that $\exists Xc$ (where $X$ is the "next" operator) holds in every state from which there exists a neighbor with $c$. Thus, for example, $1\models \exists Xc$.
Now, $\forall (\phi U \psi)$ holds if in all computations $\phi$ holds until $\psi$ holds. In particular, every state that satisfies $\psi$ also satisfies $\forall (\phi U \psi)$, since the eventuality holds immediately.
Thus, $1$ satisfies the formula. See if you can complete the rest of them now.