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

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

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.