1
$\begingroup$

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
Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

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?

Improve this answer
$\endgroup$
4
  • $\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$
    – eyes enberg
    Commented Apr 25, 2015 at 18:37
  • $\begingroup$ One problem with the current approach is the notion of the "last state" - transition systems usually contain cycles. $\endgroup$
    – Klaus Draeger
    Commented Apr 25, 2015 at 21:25
  • $\begingroup$ OK. I made further changes and also tried to include ∃, not confident that it works though $\endgroup$
    – eyes enberg
    Commented Apr 27, 2015 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$
    – Klaus Draeger
    Commented Apr 28, 2015 at 10:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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