Abstract model checking: Difference between revisions

Revision as of 10:03, 8 February 2007

Revision as of 10:00, 15 February 2007

Line 2:

{{Wikify|February 2007}}

'''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 change of values. The real state space is summarized into a smaller set of the visible ones.