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_is$, 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?
Witness for the $EU(\phi_1,\phi_2)$ using BDDs
formal methods;model checking
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.