|
|
|
| How does model checking work? |
||
| (in
brief!) |
||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| • | An
iterative algorithm that labels states in the |
||||||||||||
| transition
graph with formulae known to be true |
|||||||||||||
| • | For a
query Q |
||||||||||||
| – | the
first iteration marks all subformulae of Q of length |
||||||||||||
| 1 |
|||||||||||||
| – | the
second iteration marks them of length 2 |
||||||||||||
| – | this
terminates since the formula is finite |
||||||||||||
| • | The
details of the logic indeed matter |
||||||||||||
| – | But
not at this level of description |
||||||||||||
