| Symbolic
model checking |
|
|
|
|
|
|
|
|
|
|
|
| • | State space can be huge (>21000) for many systems |
|||||||||
| • | Key
idea: use implicit representation of state space |
|||||||||
| – | Data
structure to represent transition relation as a |
|||||||||
| boolean
formula |
||||||||||
| • | Algorithmically
manipulate the data structure to |
|||||||||
| explore
the state space |
||||||||||
| • | Key:
efficiency of the data structure |
|||||||||
