| BDD-based
model checking |
|
|
|
|
|
|
|
|
|
|
|
|
| • | Iterative,
fixed-point algorithms that are quite |
||||||||||
| similar
to those in explicit model checking |
|||||||||||
| • | Applying
boolean functions to BDDs is efficient, |
||||||||||
| which
makes the underlying algorithms efficient |
|||||||||||
| – | AND
becomes set intersection, OR becomes set union, |
||||||||||
| etc. |
|||||||||||
| • | When
the BDDs remain small, that is |
||||||||||
| – | The
ordering of the variables is a key issue |
||||||||||
