Abstract model checking
 | This article has not been added to any content categories. Please help out by adding categories to it so that it can be listed with similar articles. |
Abstraction Model checking is for systems where an actual representation is too complex and and a state space explosion will result in developing the model alone. So, the design undergoes a kind of translation to scaled down "abstract" version.
The set of variables are partitioned into visible and invisible depending on their visible change ( change of values, for instance) and the real state space is summarized into a smaller set of the visible ones.
References
- Edmund M. Clarke and Orna Grumberg and David E. Long (1992). "Model checking and abstraction". ACM Transactions on Programming Languages and Systems. 16 (5): 1512--1542.