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 (υ
_{1},…,υ
_{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 ...

Start Free Trial

No credit card required