Cheap and Secure Web Hosting Provider : See Now

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

, ,
Problem Detail:

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.

###### Asked By : eyes enberg

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.