# An algorithm to compute a set of states that satisfy a specific CTL formula

Working through a past exam question and I'm unsure where to start or what form they want the answer in:

Define an algorithm that receives as input a finite transition system TS defined over the set of actions {a, b, c} and computes the set of states of TS that satisfy the CTL formula ∃a U b.

Would anybody be able to give me a kick-start or a walk-through on how to answer this? Really appreciate any help.

edit: My attempt based on Klaus' answer

for all executions in TS
for all states
if **b** holds
add current state to the stack, EXISTS = TRUE
else if **a** holds
if current state == next state in execution
do nothing
else if next state contains **a** or **b**
add current state to the stack, EXISTS = TRUE
else
do nothing


## 1 Answer

The set of states satisfying $\exists a U b$ is the smallest set $S$ such that

• $S$ contains all states satisfying $b$, and
• $S$ contains all states satisfying $a$ which have a successor in $S$

Note that we specify the "smallest" such set because otherwise you could pick the set of all states, or include arbitrary cycles of $a$-states, etc. Do you see how to get an algorithm from this?

• Thanks for the reply. I posted my attempt as an edit of the original post - didn't take the EXISTS operator into consideration (yet) but do I have the right idea? – eyes enberg Apr 25 '15 at 18:37
• One problem with the current approach is the notion of the "last state" - transition systems usually contain cycles. – Klaus Draeger Apr 25 '15 at 21:25
• OK. I made further changes and also tried to include ∃, not confident that it works though – eyes enberg Apr 27 '15 at 14:27
• Approaching the problem in terms of executions is probably misleading - try to construct the set of states backwards, starting from the states satisfying $b$. – Klaus Draeger Apr 28 '15 at 10:55