Witness for the $EU(\phi_1,\phi_2)$ using BDDs

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?

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.

StackExchange Computer Science Q#2641, answer score: 3