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
    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?

  • $\begingroup$ 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? $\endgroup$ Apr 25 '15 at 18:37
  • $\begingroup$ One problem with the current approach is the notion of the "last state" - transition systems usually contain cycles. $\endgroup$ Apr 25 '15 at 21:25
  • $\begingroup$ OK. I made further changes and also tried to include ∃, not confident that it works though $\endgroup$ Apr 27 '15 at 14:27
  • $\begingroup$ Approaching the problem in terms of executions is probably misleading - try to construct the set of states backwards, starting from the states satisfying $b$. $\endgroup$ Apr 28 '15 at 10:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.