Handbook of Automated Reasoning

10.2 Symbolic Model Checking for CTL

In [Burch, Clarke, McMillan, Dill and Hwang 1992], the term symbolic model checking was introduced for algorithms which use a BDD representation of the Kripke model (cf. Page 1735).

Assume that the transition relation is given as a BDD over the variables $\left({\upsilon }_1,\dots ,{\upsilon }_n,{{\upsilon }^{\prime }}_1,\dots {{\upsilon }^{\prime }}_n\right)$ , and for each $\text{p}\in \mathcal{P}$ a BDD over (υ ₁,…,υ _n) is given which represents the set $\mathcal{I}\left(\text{p}\right)$ . We will show how the naive CTL model checking algorithm in Fig. 17 on P. 1714 can be implemented ...