Witness for the $EU(\phi_1,\phi_2)$ using BDDs
-
16-10-2019 - |
Question
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?
Solution
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.