Abstract model checking: Difference between revisions

Revision as of 18:42, 26 January 2007

Revision as of 18:45, 26 January 2007

Line 15:

3. If there is a counter example, then go back to the real state space and find out if it actually a counter model. <br/>

4. If not, return and continue model checking. <br/>

<br/>

Spurious examples are mostly generated because dead end states and bad states are abstracted to the same kind. To solve this we need to create a segregation between the 2 kinds.

==References==

* {{cite journal | author=Edmund M. Clarke and Orna Grumberg and David E. Long | title=Model checking and abstraction | journal=ACM Transactions on Programming Languages and Systems| year=1992| volume=16 | issue=5 | pages=1512--1542}}