I wanted ask if you know an algorithm to find the witness for $EU(\phi_1,\phi_2)$ (CTL formula "Exist Until") using BDDs (Binary Decision Diagram). In pratice you should use the fixed point for calculating $EU(\phi_1,\phi_2)$, that is:

$\qquad \displaystyle EU(\phi_1,\phi_2)=\mu.Q (\phi_2 \vee (\phi_1 \wedge EX Q)) $

Unwinding the recursion, we get:

$\qquad \displaystyle \begin{align} Q_0 &= \textrm{false} \\ Q_1 &= \phi_2 \\ Q_2 &= \phi_2 \vee (\phi_1 \wedge EX \phi_2) \\ \ \vdots \end{align}$

and so on.

To generate a witness (path) we can do a forward reachability check within the sequence of $Q_i’s$, that is find a path

$\qquad \displaystyle \pi= s_1 \rightarrow s_2 \rightarrow \cdots \rightarrow s_n$

such that $s_i \in Q_{n-i} \cap R(s_{i-1})$ (where $R(s_{i-1})= \{ s \mid R(s_{i-1},s) \}$ and $R(s_{i-1},s$) is the transition from $s_{i-1}$ to $s$ ) where $s_0 \in Q_n $ and $s_n \in Q_1=\phi_2$.

How you can do this with BDDs?

  • 1
    $\begingroup$ 1) What is $Q$? 2) What is $EX$? 3) What is $R(s_{i-1},s)$? $\endgroup$
    – Raphael
    Commented Jul 9, 2012 at 9:01
  • $\begingroup$ Q is a set of states, $EX$ is the CTL formula "exist next", and $R$ is the transition function. $\endgroup$
    – kafka
    Commented Jul 9, 2012 at 9:53
  • $\begingroup$ Aha, so it's CTL over some transition system defined by $Q$ and $R$. That was not at all clear without context. $\endgroup$
    – Raphael
    Commented Jul 9, 2012 at 9:54

1 Answer 1


What you describe is symbolic model checking, and it is treated in this set of slides, using reduced ordered BDDs.

In a nutshell, you still do the fixpoint iteration, the main issue being how to do the transformation $Q\mapsto \phi_2\vee(\phi_1\wedge EXQ)$ on BDDs. The elementary operations you need are renaming (to replace unprimed by primed variables in $Q$, obtaining $Q'$), boolean operations (to form $\phi_2\vee(\phi_1\wedge R\wedge Q')$) and abstraction (to do existential quantifier elimination on the primed variables). The witness generation can then be done similarly forwards from the initial states, requiring at step $i$ that $s_i$ is in $Q_{n-i}$ as you did above.


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.