# 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


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?
• Approaching the problem in terms of executions is probably misleading - try to construct the set of states backwards, starting from the states satisfying $b$. Apr 28 '15 at 10:55