# 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.

• "Grade my answer" questions are not a good fit for this site; answers are not likely to help future visitors. Please read related meta discussions here and here and adjust your question accordingly, e.g. by formulating a specific question about a single element of your answer you are uncertain about, or better yet, asking a more general conceptual question. If you just want general feedback, you're welcome to visit Computer Science Chat. – D.W. Apr 30 '15 at 22:50

## 1 Answer

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.

• Thanks, this cleared a few things up. So based on this explanation, I ended up with only states 1 and 4 satisfying the formula. Do you agree with this? – eyes enberg Apr 27 '15 at 15:37
• Nope. 2,3 and 6 also satisfy it, but I'll leave it to you to think why. – Shaull Apr 27 '15 at 16:12
• Ah yeah, don't know why I ruled them out. Thanks – eyes enberg Apr 27 '15 at 19:13
• Do you know the rule used to remove a state from a TS? If I wanted to remove state 5 do I simply remove the arrows going in and out of the state or also including the arrow from 6 to 4 (since it forms a cycle for 5)? – eyes enberg Apr 27 '15 at 19:16
• Typically when you remove a state from a graph, you just remove all incoming and outgoing edges, nothing else. – Shaull Apr 27 '15 at 19:18