Abstract model checking: Difference between revisions

Revision as of 19:05, 26 January 2007

Revision as of 19:18, 26 January 2007

Line 16:

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. The next step is to find the subset of invisible variables that actually make a difference between the dead end and bad states and add this subset to the set of visible or monitored variables. If the seperation proves expensive, refinement could be based on learning from samples.

==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}}